proposition: Lemma picard_sy (f : UniformlyContinuous sx sy) (x : sx) : ball (proj1_sig ry) y0 (picard'' f x).
proof: Proof. destruct x as [x x_sx]. unfold picard''; simpl. unfold restrict, Basics.compose; simpl. unfold picard'. apply mspc_ball_CRabs. assert (forall b, CRabs (y0 - (y0 + b)) == abs b)%CR. { intro b. pose proof (CRabs_negate b). rewrite <- H0. apply CRabs_wd. transitivity (y0 + (-y0-b)). apply ucFun2_wd. reflexivity. exact (CRopp_plus_distr y0 b). rewrite plus_assoc. rewrite rings.plus_negate_r, rings.plus_0_l. reflexivity. } unfold abs, abs_sig, proj1_sig, CR_abs. unfold negate, plus. rewrite H0. clear H0. transitivity ('(abs (x - x0) * M)). + apply int_abs_bound; [apply _ |]. intros t A. assert (@mspc_ball Q (msp_mspc_ball Q_as_MetricSpace) (proj1_sig rx) x0 t) as A1. apply (mspc_ball_convex x0 x). apply (@mspc_refl Q). exact (msp_mspc_ball_ext Q_as_MetricSpace). apply (proj2_sig rx). trivial. trivial. apply (extend_inside (Y:=CR)) in A1. destruct A1 as [p A1]. specialize (A1 (v ∘ together Datatypes.id f ∘ diag)). pose proof (CRabs_wd _ _ A1). rewrite H0. clear H0. apply bounded. + apply CRle_Qle. change (abs (x - x0) * M ≤ proj1_sig ry). transitivity (`rx * M). - now apply (orders.order_preserving (.* M)), mspc_ball_Qabs_flip. - apply rx_M. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.reals.CRreal Coq.Unicode.Utf8 Coq.Program.Program CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs CoRN.tactics.Qauto Coq.QArith.Qround CoRN.model.metric2.Qmetric  CoRN.ode.metric CoRN.ode.FromMetric2 CoRN.ode.AbstractIntegration CoRN.ode.SimpleIntegration CoRN.ode.BanachFixpoint MathClasses.interfaces.canonical_names MathClasses.misc.decision MathClasses.misc.setoid_tactics MathClasses.misc.util MathClasses.implementations.stdlib_rationals MathClasses.theory.rationals