proposition: Theorem neq_0_r n : n ~= 0 <-> exists m, n == S m.
proof: Proof. cases n. - split; intro H;[now elim H | destruct H as [m H]; symmetry in H; false_hyp H neq_succ_0]. - intro n; split; intro H; [now exists n | apply neq_succ_0]. Qed.
imports: Decidable NAxioms NZProperties