theorem sucne0 (a b: nat): $ a = suc b -> a != 0 $;
suc b != 0
a = suc b -> (a != 0 <-> suc b != 0)
a = suc b -> a != 0