proposition: Lemma less_nring : forall n m : nat, nring (R:=R) n [<] nring m -> n < m.
proof: Proof. intro n; induction n as [| n Hrecn]. intros m H. induction m as [| m Hrecm]. exfalso; generalize H; apply less_irreflexive_unfolded. auto with arith. intros m H. induction m as [| m Hrecm]. exfalso. cut (nring (R:=R) 0 [<] nring (S n)). apply less_antisymmetric_unfolded; assumption. apply nring_less; auto with arith. cut (n < m). auto with arith. apply Hrecn. rstepr (nring (R:=R) m[+][1][-][1]). apply shift_less_minus. apply H. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)