proposition: Lemma pos_nring_S : forall n, ZeroR [<] nring (S n).
proof: Proof. simple induction n; simpl in |- *; intros. astepr OneR; apply pos_one. apply less_leEq_trans with (nring (R:=R) n0[+][1]). assumption. apply less_leEq. apply less_plusOne. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)