proposition: Lemma nring_less_succ : forall m : nat, (nring m:R) [<] nring (S m).
proof: Proof. intro m. simpl in |- *. astepr ([1][+]nring (R:=R) m). astepl ([0][+]nring (R:=R) m). apply plus_resp_less_rht. apply pos_one. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)