proposition: Lemma nat_less_bin_nexp : forall p : nat, Snring R p [<] Two[^]S p.
proof: Proof. intro n. unfold Snring in |- *. induction n as [| n Hrecn]. simpl in |- *. astepl ([1]:R). astepr (([0]:R) [+][1][+][1]). astepr (([1]:R) [+][1]). astepr (Two:R). apply one_less_two. astepl (nring (R:=R) (S n) [+][1]). astepr ((Two:R)[^]S n[*]Two). astepr ((Two:R)[^]S n[*][1][+]Two[^]S n[*][1]). apply plus_resp_less_both. astepr ((Two:R)[^]S n). exact Hrecn. astepr ((Two:R)[^]S n). astepl (([1]:R)[^]S n). apply nexp_resp_less. intuition. apply less_leEq. apply pos_one. apply one_less_two. rational. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)