proposition: Lemma bin_less_un : forall n H H1, ([1][/] (Two:R) [^]S n[//]H) [<] ([1][/] nring (S n) [//]H1).
proof: Proof. intros n H H1. apply recip_resp_less. simpl in |- *. apply plus_resp_nonneg_pos. apply nring_nonneg. apply pos_one. induction n as [| n Hrecn]. simpl in |- *. astepl ([1]:R). astepr (([1]:R)[+][1]). astepr (Two:R). apply one_less_two. rational. astepr ((Two:R)[*]Two[^]S n). apply leEq_less_trans with ((Two:R)[*]nring (S n)). apply suc_leEq_dub. apply mult_resp_less_lft. apply Hrecn. red; unfold f_rcpcl'. apply nexp_resp_ap_zero. apply Greater_imp_ap. apply pos_two. red; unfold f_rcpcl'. apply nring_ap_zero. auto. apply pos_two. Qed.
imports: Coq.Arith.Arith CoRN.algebra.COrdCauchy Coq(Lia)