theorem le02 (a: nat): $ a <= 0 <-> a = 0 $;
0 <= a
a <= 0 -> 0 <= a -> a = 0
a <= 0 -> a = 0
a = 0 -> a <= 0
a <= 0 <-> a = 0