proposition: Lemma binom_ineq (a : Q) (n : nat) : -1 ≤ a -> 1 + (inject_Z n) * a ≤ (1 + a)^n.
proof: Proof. intro A. assert (A1 : 0 ≤ 1 + a) by (now apply (order_preserving (1 +)) in A; rewrite plus_negate_r in A). induction n as [| n IH] using nat_induction. + rewrite nat_pow_0; change (1 + 0 * a ≤ 1); now rewrite mult_0_l, plus_0_r. + rewrite nat_pow_S. transitivity ((1 + a) * (1 + (inject_Z n) * a)). - rewrite Nat2Z.inj_add, inject_Z_plus. stepr (1 + (1 + (inject_Z n)) * a + (inject_Z n) * a²) by ring. apply nonneg_plus_le_compat_r. apply nonneg_mult_compat; [solve_propholds | apply square_nonneg]. - now apply (order_preserving ((1 + a) *.)) in IH. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.QArith.QArith MathClasses.implementations.stdlib_rationals CoRN.model.structures.Qinf CoRN.model.structures.Qpossec CoRN.model.structures.QposInf CoRN.model.structures.QnonNeg MathClasses.interfaces.abstract_algebra MathClasses.implementations.QType_rationals MathClasses.interfaces.additional_operations CoRN.tactics.Qauto Coq.QArith.QOrderedType MathClasses.theory.rings MathClasses.theory.dec_fields MathClasses.orders.rings MathClasses.orders.dec_fields MathClasses.theory.nat_pow MathClasses.interfaces.naturals MathClasses.interfaces.orders CoRN.reals.fast.CRGeometricSum CoRN.ode.metric