let i be Nat; :: thesis: ( i divides 0 & 1 divides i )
0 = i * 0 ;
hence i divides 0 ; :: thesis: 1 divides i
i = i * 1 ;
hence 1 divides i ; :: thesis: verum