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