proposition: Lemma reverse_iso_bin_wd_fun : forall (f:Cauchy_IR -> Cauchy_IR -> Cauchy_IR) (g:CR -> CR -> CR), (forall w x, (w == x)%CR -> forall y z, (y == z -> g w y == g x z)%CR) -> (forall (x y:Cauchy_IR), (g (Cauchy_IRasCR x) (Cauchy_IRasCR y) == Cauchy_IRasCR (f x y))%CR) -> forall (x y:CR), (f (CRasCauchy_IR x) (CRasCauchy_IR y) [=] CRasCauchy_IR (g x y)).
proof: Proof. intros f g g_wd H x y. stepl (CRasCauchy_IR (Cauchy_IRasCR (f (CRasCauchy_IR x) (CRasCauchy_IR y)))); [| apply Cauchy_IRasCauchy_IR]. apply CRasCauchy_IR_wd. symmetry. transitivity (g (Cauchy_IRasCR (CRasCauchy_IR x)) (Cauchy_IRasCR (CRasCauchy_IR y))); [|apply H]. apply g_wd; symmetry; apply CRasCR. 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