let a, b be Nat; :: thesis: (((a * b) + 1) choose 1) mod b = 1 mod b

per cases ( a is zero or b is zero or ( not a is zero & not b is zero ) ) ;

suppose ( a is zero or b is zero ) ; :: thesis: (((a * b) + 1) choose 1) mod b = 1 mod b

hence (((a * b) + 1) choose 1) mod b = 1 mod b ; :: thesis: verum

end;

suppose B1: ( not a is zero & not b is zero ) ; :: thesis: (((a * b) + 1) choose 1) mod b = 1 mod b

then reconsider a = a as non zero Nat ;
reconsider b = b as non zero Nat by B1;
(((a * b) + 1) choose (0 + 1)) mod b = (((a * b) choose 0) + ((a * b) choose (0 + 1))) mod b by NEWTON:22
.= ((((a * b) choose 0) mod b) + (((a * b) choose 1) mod b)) mod b by NAT_D:66
.= ((((a * b) choose 0) mod b) + 0) mod b by ILO
.= (1 mod b) mod b by NEWTON:19 ;
hence (((a * b) + 1) choose 1) mod b = 1 mod b ; :: thesis: verum

end;

end;