theorem mod12 (a: nat): $ a % 1 = 0 $;
a % 1 < 1 <-> a % 1 = 0
1 != 0 -> a % 1 < 1
1 != 0
a % 1 < 1
a % 1 = 0