proposition: Lemma cauchy_x : cauchy x (λ e, Z.to_nat (Qceiling (d / (e * (1 - q)²))%mc)).
proof: Proof. assert (d_nonneg : 0 ≤ d) by solve_propholds. assert (d_pos_0 : 0 = d \/ 0 < d) by now apply le_equiv_lt. destruct d_pos_0 as [d_0 | d_pos]; [now apply const_x |]. intros e e_pos. match goal with |- forall m n, @?G m n => intros m n; assert (A : forall m n, m ≤ n -> G m n) end. + clear m n; intros m n le_m_n A _. rewrite <- (cut_minus_le n m); trivial. rewrite plus_comm. apply (mspc_monotone (d * q^m / (1 - q))%mc); [| apply dist_xm_xn']. cut (q ^ m ≤ e * (1 - q) / d). - intro A1. apply (order_preserving (d *.)), (order_preserving (.* /(1 - q))) in A1. apply (po_proper' A1); [easy | field; split; solve_propholds]. - apply power_tends_to_zero; [solve_propholds |]. apply (po_proper' A); [| easy]. apply f_equal, Qceiling_comp. match goal with |- (Qeq ?l ?r) => change (l = r) end. field; repeat split; solve_propholds. + assert (A1 : TotalRelation (A := nat) (≤)) by apply _; destruct (A1 m n). - now apply A. - intros; apply mspc_symm; now apply A. 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