let k be Nat; :: thesis: for n being non zero Nat st (k + 1) mod n = 0 holds
(k + 1) div n = (k div n) + 1
let n be non zero Nat; :: thesis: ( (k + 1) mod n = 0 implies (k + 1) div n = (k div n) + 1 )
assume A1: (k + 1) mod n = 0 ; :: thesis: (k + 1) div n = (k div n) + 1
n >= 1 by NAT_1:14;

per cases then ( n = 1 or n > 1 ) by XXREAL_0:1;

suppose n = 1 ; :: thesis: (k + 1) div n = (k div n) + 1

then ( (k + 1) div n = k + 1 & k div n = k & 1 div n = 1 ) by NAT_2:4;
hence (k + 1) div n = (k div n) + 1 ; :: thesis: verum

end;

suppose B1: n > 1 ; :: thesis: (k + 1) div n = (k div n) + 1

n divides k + 1 by A1, PEPIN:6;
then reconsider k = k as non zero Nat by B1, NAT_D:7;
B2: ((k + 1) - 1) mod n = n - 1 by A1, ND1;
B3: n mod n = 0 ;
B4: ( ((k div n) * n) div n = k div n & (1 * n) div n = 1 ) by NAT_D:18;
(1 + k) div n = (1 + (((k div n) * n) + (k mod n))) div n by NAT_D:2
.= (n + ((k div n) * n)) div n by B2
.= (k div n) + 1 by B3, B4, NAT_D:19 ;
hence (k + 1) div n = (k div n) + 1 ; :: thesis: verum

end;

end;