proposition: Lemma dist_xm_xn : forall m n : nat, ball (d * q^m * (1 - q^n) / (1 - q)) (x m) (x (m + n)).
proof: Proof. intro m; induction n as [| n IH] using nat_induction. + rewrite right_identity; apply mspc_refl. now rewrite nat_pow_0, plus_negate_r, right_absorb, left_absorb. + apply (mspc_triangle' (d * q^m * (1 - q^n) / (1 - q))%mc (d * q^(m + n))%mc (x (m + n))); trivial. - rewrite nat_pow_S, nat_pow_exp_plus. field; solve_propholds. - mc_setoid_replace (m + (1 + n)) with (1 + (m + n)) by ring. apply dist_xn_xSn. 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