let a, b, c be Nat; :: thesis: ((a + 1) choose (b + 1)) mod c = (((a choose b) mod c) + ((a choose (b + 1)) mod c)) mod c
((a + 1) choose (b + 1)) mod c = ((a choose b) + (a choose (b + 1))) mod c by NEWTON:22
.= (((a choose b) mod c) + ((a choose (b + 1)) mod c)) mod c by NAT_D:66 ;
hence ((a + 1) choose (b + 1)) mod c = (((a choose b) mod c) + ((a choose (b + 1)) mod c)) mod c ; :: thesis: verum