N+
The positive natural numbers have some nice properties. Addition as well as multiplication preserve the feature of being positive.Lemma plus_resp_Npos0 : forall x y : N, x <> 0 -> y <> 0 -> (x+y) <> 0.
Lemma Npos_is_suc : forall y : N, y <> 0 -> exists m : N, y = S m.
Lemma mult_resp_Npos0 : forall x y : N, x <> 0 -> y <> 0 -> (x*y) <> 0.