Lemma natAddNonzero : forall (n m : nat), 0 <> n -> 0 <> m + n.
