proposition: Lemma const_x (N : Q -> nat) : d = 0 -> cauchy x N.
proof: Proof. intro eq_d_0. assert (A := mspc_distance (x 0) (x 1)). subst d; rewrite eq_d_0 in A. assert (C : forall n, x n = x 0). + induction n as [| n IH] using nat_induction; [easy |]. change (x (1 + n)) with (f (x n)). rewrite IH. symmetry; apply A. + intros e e_pos m n _ _. rewrite (C m), (C n). apply mspc_refl. 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