fact: Fixpoint CompactImproveApproximation (s:Compact X) (k d e:Qpos) (pt:X) (Hpt : InFinEnumC pt (approximate s d)) (n : nat) { struct n } : X := match n with | O => pt | S p => let (f,_) := HausdorffBallHausdorffBallStrong locatedX (regFun_prf s d (k*d)%Qpos) in let (pt',HptX) := f pt Hpt e in let (Hpt',_) := HptX in @CompactImproveApproximation s k (k*d) (k*e) pt' Hpt' p end.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Limit CoRN.metric2.FinEnum Coq.ZArith.Zpow_facts CoRN.metric2.Complete CoRN.logic.Classic Coq.QArith.Qpower Coq.QArith.Qround