let n be non zero Nat; :: thesis: for k, l being Nat st k mod n = l mod n & k > l holds
ex s being Integer st k = l + (s * n)
let k, l be Nat; :: thesis: ( k mod n = l mod n & k > l implies ex s being Integer st k = l + (s * n) )
assume that
A1: k mod n = l mod n and
A2: k > l ; :: thesis: ex s being Integer st k = l + (s * n)
consider m being Nat such that
A3: k = l + m by A2, NAT_1:10;
take m div n ; :: thesis: k = l + ((m div n) * n)
( l = ((l div n) * n) + (l mod n) & k = ((k div n) * n) + (l mod n) ) by A1, NAT_D:2;
then m mod n = (((k div n) - (l div n)) * n) mod n by A3
.= 0 by Th20 ;
then (l + m) div n = (l div n) + (m div n) by NAT_D:19;
then k = (((l div n) + (m div n)) * n) + (l mod n) by A1, A3, NAT_D:2
.= ((m div n) * n) + (((l div n) * n) + (l mod n))
.= ((m div n) * n) + l by NAT_D:2 ;
hence k = l + ((m div n) * n) ; :: thesis: verum