proposition: Lemma reverse_iso_wd_fun : forall (f:Cauchy_IR -> Cauchy_IR) (g:CR -> CR), (forall x y, (x==y -> g x == g y)%CR) -> (forall (x:Cauchy_IR), (g (Cauchy_IRasCR x) == Cauchy_IRasCR (f x))%CR) -> forall (x:CR), (f (CRasCauchy_IR x) [=] CRasCauchy_IR (g x)).
proof: Proof. intros f g g_wd H x. stepl (CRasCauchy_IR (Cauchy_IRasCR (f (CRasCauchy_IR x)))); [| apply Cauchy_IRasCauchy_IR]. apply CRasCauchy_IR_wd. symmetry. transitivity (g (Cauchy_IRasCR (CRasCauchy_IR x))). apply g_wd. symmetry. apply CRasCR. apply H. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.model.reals.Cauchy_IR CoRN.tactics.CornTac Coq(Lia) CoRN.model.metric2.Qmetric CoRN.model.totalorder.QMinMax Coq.QArith.Qabs CoRN.reals.fast.CRFieldOps