let n, k1, k2 be Nat; :: thesis: ( n <> 0 & k1 mod n = k2 mod n & k1 <= k2 implies ex t being Nat st k2 - k1 = n * t )
assume that
A1: n <> 0 and
A2: k1 mod n = k2 mod n and
A3: k1 <= k2 ; :: thesis: ex t being Nat st k2 - k1 = n * t
consider t being Integer such that
A4: t = (k2 div n) - (k1 div n) ;
k2 div n >= k1 div n by A3, NAT_2:24;
then (k2 div n) - (k1 div n) >= (k1 div n) - (k1 div n) by XREAL_1:9;
then reconsider t = t as Element of NAT by A4, INT_1:3;
take t ; :: thesis: k2 - k1 = n * t
( k1 = (n * (k1 div n)) + (k1 mod n) & k2 = (n * (k2 div n)) + (k2 mod n) ) by A1, NAT_D:2;
hence k2 - k1 = n * t by A2, A4; :: thesis: verum