let k, n be Nat; :: thesis: ( n <= k & k < n + n implies k div n = 1 )
assume that
A1: n <= k and
A2: k < n + n ; :: thesis: k div n = 1
A3: k = n + (k - n)
.= (n * 1) + (k -' n) by A1, XREAL_1:233 ;
k - n < (n + n) - n by A2, XREAL_1:9;
hence k div n = 1 by A3, NAT_D:def 1; :: thesis: verum