let n be Nat; :: thesis: for m being non zero Nat holds
( (n mod m) choose (m - 1) = 1 iff n mod m = m - 1 )
let m be non zero Nat; :: thesis: ( (n mod m) choose (m - 1) = 1 iff n mod m = m - 1 )
( n mod m <> m - 1 implies (n mod m) choose (m - 1) = 0 )

proof

assume B1: n mod m <> m - 1 ; :: thesis: (n mod m) choose (m - 1) = 0
n mod m < (m - 1) + 1 by NAT_D:1;
then n mod m <= m - 1 by INT_1:7;
then n mod m < m - 1 by B1, XXREAL_0:1;
hence (n mod m) choose (m - 1) = 0 by NEWTON:def 3; :: thesis: verum

end;

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