proposition: Lemma very_weak_binomial : forall (OF : COrdField) (x : OF) (n : nat), [0][<]x -> 1 < n -> [1][+]nring n[*]x[<](x[+][1])[^]n.
proof: Proof. do 3 intro. intros H H0. induction n as [| n Hrecn]. apply False_rect. apply (Nat.nlt_0_r 0). apply Nat.lt_trans with (m := 1). apply Nat.lt_0_succ. assumption. case (le_lt_eq_dec 2 (S n) (proj1 (Nat.le_succ_l 1 (S n)) H0)). intro. cut ([1][+]nring n[*]x[<](x[+][1])[^]n). intro. apply less_wdr with (y := (x[+][1])[^]n[*](x[+][1])). apply less_transitive_unfolded with (y := [1][+]nring (S n)[*]x[+]nring n[*]x[^]2). apply plus_cancel_less with (z := [--]([1][+]nring (S n)[*]x)). rstepl ([0]:OF). rstepr (nring n[*]x[^]2). apply mult_resp_pos. change (nring (R:=OF) 0[<]nring n) in |- *. apply nring_less. apply Nat.succ_lt_mono. assumption. apply pos_square. apply Greater_imp_ap. assumption. apply less_wdl with (x := ([1][+]nring n[*]x)[*](x[+][1])). apply mult_resp_less. assumption. apply less_transitive_unfolded with (y := x). assumption. apply less_plusOne. simpl in |- *. rational. simpl in |- *. apply eq_reflexive_unfolded. apply Hrecn. apply Nat.succ_lt_mono. assumption. intro H1. rewrite <- H1. apply less_wdr with (y := [1][+]Two[*]x[+]x[^]2). apply plus_cancel_less with (z := [--]([1][+]Two[*]x)). astepl ([0]:OF). apply less_wdr with (y := x[^]2). apply pos_square. apply Greater_imp_ap. assumption. rational. simpl in |- *. rational. Qed.
imports: CoRN.reals.iso_CReals CoRN.algebra.Expon