let n be non empty 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 A1: ( k mod n = l mod n & k > l ) ; :: thesis: ex s being Integer st k = l + (s * n)
A2: l = ((l div n) * n) + (l mod n) by NAT_D:2;
A3: k = ((k div n) * n) + (l mod n) by A1, NAT_D:2;
consider m being Nat such that
A4: k = l + m by A1, NAT_1:10;
m mod n = (((k div n) - (l div n)) * n) mod n by A2, A3, A4
.= 0 by Th20 ;
then (l + m) div n = (l div n) + (m div n) by NAT_D:19;
then A5: k = (((l div n) + (m div n)) * n) + (l mod n) by A1, A4, NAT_D:2
.= ((m div n) * n) + (((l div n) * n) + (l mod n))
.= ((m div n) * n) + l by NAT_D:2 ;
take m div n ; :: thesis: k = l + ((m div n) * n)
thus k = l + ((m div n) * n) by A5; :: thesis: verum