proposition: Lemma nring_less : forall m n : nat, m < n -> (nring m:R) [<] nring n.
proof: Proof. intros m n H. generalize (toCProp_lt _ _ H); intro H0. elim H0. apply nring_less_succ. clear H0 H n; intros n H H0. apply less_transitive_unfolded with (nring (R:=R) n). assumption. apply nring_less_succ. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)