proposition: Lemma suc_leEq_dub : forall n, nring (R:=R) (S (S n)) [<=] Two[*]nring (S n).
proof: Proof. intro n. induction n as [| n Hrecn]. apply eq_imp_leEq. rational. astepl (nring (R:=R) (S (S n)) [+]nring 1). apply leEq_transitive with (nring (R:=R) 2[*]nring (S n) [+]nring 1). apply plus_resp_leEq. astepr ((Two:R) [*]nring (S n)). exact Hrecn. simpl in |- *. astepr ((([0]:R) [+][1][+][1]) [*] (nring n[+][1]) [+] (([0]:R) [+][1][+][1]) [*][1]). apply plus_resp_leEq_lft. astepr (([0]:R) [+][1][+][1]). astepr (([0]:R) [+] ([1][+][1])). apply plus_resp_leEq_lft. astepr (Two:R). apply less_leEq. apply one_less_two. simpl in |- *. astepl (nring (R:=R) n[+][1][+] ([1][+] ([0][+][1]))). astepl (nring (R:=R) n[+] ([1][+] ([1][+] ([0][+][1])))). astepr (nring (R:=R) n[+][1][+] ([1][+][1])). astepr (nring (R:=R) n[+] ([1][+] ([1][+][1]))). rational. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)