proposition: Lemma power_big' : forall (R : COrdField) (x : R) n, [0] [<=] x -> [1][+]nring n[*]x [<=] ([1][+]x) [^]n.
proof: Proof. intros. induction n as [| n Hrecn]; intros. rstepl ([1]:R). astepr ([1]:R). apply leEq_reflexive. simpl in |- *. apply leEq_transitive with (([1][+]nring n[*]x) [*] ([1][+]x)). rstepr ([1][+] (nring n[+][1]) [*]x[+]nring n[*]x[^]2). astepl ([1][+] (nring n[+][1]) [*]x[+][0]). apply plus_resp_leEq_lft. apply mult_resp_nonneg. astepl (nring 0:R). apply nring_leEq. auto with arith. apply sqr_nonneg. apply mult_resp_leEq_rht. auto. apply less_leEq. astepl (([0]:R) [+][0]). apply plus_resp_less_leEq. apply pos_one. auto. Qed.
imports: CoRN.reals.Max_AbsIR CoRN.algebra.Expon CoRN.algebra.CPoly_ApZero