proposition: Lemma poly : forall (n:nat) (x:R), 0 < x -> 1 + INR n * x <= (1 + x) ^ n.
proof: Proof. intros; elim n. - simpl; cut (1 + 0 * x = 1). + intro; rewrite H0; unfold Rle; right; reflexivity. + ring. - intros; unfold pow; fold pow; apply (Rle_trans (1 + INR (S n0) * x) ((1 + x) * (1 + INR n0 * x)) ((1 + x) * (1 + x) ^ n0)). + cut ((1 + x) * (1 + INR n0 * x) = 1 + INR (S n0) * x + INR n0 * (x * x)). * intro; rewrite H1; pattern (1 + INR (S n0) * x) at 1; rewrite <- (let (H1, H2) := Rplus_ne (1 + INR (S n0) * x) in H1); apply Rplus_le_compat_l; elim n0; intros. -- simpl; rewrite Rmult_0_l; unfold Rle; right; auto. -- unfold Rle; left; generalize Rmult_gt_0_compat; unfold Rgt; intro; fold (Rsqr x); apply (H3 (INR (S n1)) (Rsqr x) (lt_INR_0 (S n1) (Nat.lt_0_succ n1))); fold (x > 0) in H; apply (Rlt_0_sqr x (Rlt_dichotomy_converse x 0 (or_intror (x < 0) H))). * rewrite (S_INR n0); ring. + unfold Rle in H0; elim H0; intro. * unfold Rle; left; apply Rmult_lt_compat_l. -- rewrite Rplus_comm; apply (Rplus_le_lt_0_compat _ _ (Rlt_le 0 x H)); apply Rlt_0_1. -- assumption. * rewrite H1; unfold Rle; right; trivial. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac