proposition: Lemma Npos_is_suc : forall y : nat, y <> 0 -> exists m : nat, y = S m.
proof: Proof. intros y H. exists (pred y). unfold pred in |- *. induction y as [| y Hrecy]. intuition. intuition. Qed.
imports: CoRN.model.structures.Nsec Coq(Arith Lia)