proposition: Lemma power_tends_to_zero (e : Q) (n : nat) : 0 < e -> Z.to_nat (Qceiling (/(e * (1 - q)))%mc) ≤ n -> q ^ n ≤ e.
proof: Proof. intros A1 A2. assert (A3 : 0 < n). + let T := type of A2 in match T with (?lhs ≤ _) => apply lt_le_trans with (y := lhs) end; [| trivial]. apply Q.Qlt_lt_of_nat_inject_Z; change (0 < / (e * (1 - q))); solve_propholds. + destruct n as [| n]; [elim (Nat.lt_irrefl _ A3) |]. rewrite <- Qpower_mc_power. apply GeometricCovergenceLemma with (e := e ↾ A1); [solve_propholds .. |]. apply (Q.le_Qle_Qceiling_to_nat _ (S n)), A2. 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