proposition: Lemma reverse_iso_bin_uc_fun : forall (f:Cauchy_IR -> Cauchy_IR -> Cauchy_IR) (g:CR --> CR --> 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 H x y. apply (reverse_iso_bin_wd_fun f (ucFun2 g)). apply ucFun2_wd. assumption. 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