proposition: Lemma nring_leEq : forall m n : nat, m <= n -> (nring m:R) [<=] nring n.
proof: Proof. intros m n H. elim (le_lt_eq_dec _ _ H); intro H1. rewrite -> leEq_def in |- *. apply less_antisymmetric_unfolded. apply nring_less. auto. rewrite H1. rewrite -> leEq_def in |- *. apply less_irreflexive_unfolded. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)