let n be Nat; :: thesis: for m being non zero Nat holds (n mod m) choose (m - 1) < 2
let m be non zero Nat; :: thesis: (n mod m) choose (m - 1) < 2
n mod m < (m - 1) + 1 by NAT_D:1;
then n mod m <= m - 1 by INT_1:7;

per cases then ( n mod m = m - 1 or n mod m < m - 1 ) by XXREAL_0:1;

suppose n mod m = m - 1 ; :: thesis: (n mod m) choose (m - 1) < 2

then (n mod m) choose (m - 1) = 1 by NEWTON:21;
hence (n mod m) choose (m - 1) < 2 ; :: thesis: verum

end;

suppose n mod m < m - 1 ; :: thesis: (n mod m) choose (m - 1) < 2

hence (n mod m) choose (m - 1) < 2 by NEWTON:def 3; :: thesis: verum

end;

end;