let a, b be non zero Nat; :: thesis: ((a * b) choose 1) mod b = 0
((a * b) choose 1) mod b = (0 + (a * b)) mod b ;
hence ((a * b) choose 1) mod b = 0 ; :: thesis: verum