proposition: Lemma iter_fixpoint `{ExtMetricSpaceClass X, ExtMetricSpaceClass Y} (f : X -> X) {mu : Q -> Qinf} {_ : IsUniformlyContinuous f mu} (x : seq X) (a : X) (N : Q -> nat) : (forall n : nat, x (S n) = f (x n)) -> seq_lim x a N -> f a = a.
proof: Proof. intros A1 A2; generalize A2; intro A3. apply seq_lim_S in A2. apply (seq_lim_cont f) in A3. setoid_replace (x ∘ S) with (f ∘ x) in A2 by (intros ? ? eqmn; rewrite eqmn; apply A1). eapply seq_lim_unique; eauto. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.QArith.QArith MathClasses.theory.setoids MathClasses.theory.products MathClasses.implementations.stdlib_rationals 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