proposition: Lemma leEq_nring : forall n m, nring (R:=R) n [<=] nring m -> n <= m.
proof: Proof. intro n; induction n as [| n Hrecn]. intros. auto with arith. intros. induction m as [| m Hrecm]. exfalso. cut (nring (R:=R) n [<] [0]). change (Not (nring (R:=R) n[<](nring 0))). rewrite <- leEq_def. apply nring_leEq. auto with arith. change (nring n [<] nring (R:=R) 0) in |- *. apply nring_less. apply Nat.lt_le_trans with (S n). auto with arith. exfalso. revert H; rewrite -> leEq_def. intro H; destruct H. apply nring_less; auto with arith. cut (n <= m). auto with arith. apply Hrecn. rstepr (nring (R:=R) m[+][1][-][1]). apply shift_leEq_minus. apply H. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)