proposition: Lemma dist_xm_xn' : forall m n : nat, ball (d * q^m / (1 - q)) (x m) (x (m + n)).
proof: Proof. intros m n. apply (mspc_monotone (d * q^m * (1 - q^n) / (1 - q))%mc); [| apply dist_xm_xn]. apply (order_preserving (.* /(1 - q))). rewrite <- associativity. apply (order_preserving (d *.)). rewrite <- (mult_1_r (q^m)) at 2. apply (order_preserving (q^m *.)). rewrite <- (plus_0_r 1) at 2. apply (order_preserving (1 +)). rewrite <- negate_0. apply flip_le_negate. solve_propholds. 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