proposition: Lemma CRinvT_wd : forall (x y:CR) x_ y_, (x == y -> CRinvT x x_ == CRinvT y y_)%CR.
proof: Proof. assert (X:forall x, (0 + x == x)%CR). intros x. transitivity (doubleSpeed x);[|apply doubleSpeed_Eq]. apply regFunEq_equiv, regFunEq_e. intros e. simpl. unfold Cap_raw; simpl. rewrite Qplus_0_l. apply Qball_Reflexive. apply (Qpos_nonneg (e+e)). assert (Y:forall x, (x + - 0 == x)%CR). intros x. transitivity (doubleSpeed x);[|apply doubleSpeed_Eq]. apply regFunEq_equiv, regFunEq_e. intros e. simpl. unfold Cap_raw; simpl. rewrite Qplus_0_r. apply Qball_Reflexive. apply (Qpos_nonneg (e+e)). intros x y [[c x_]|[c x_]] [[d y_]|[d y_]] H. change (-(CRinv_pos c (-x))== (-(CRinv_pos d (-y))))%CR. rewrite -> H in *. rewrite -> X in *. intros. apply CRopp_wd. destruct (Qle_total (proj1_sig c) (proj1_sig d)); [|symmetry]; apply CRinv_pos_weaken; try assumption. assert (0 < proj1_sig c) as cpos. { destruct c; exact q. } elim (Qlt_not_le _ _ cpos). rewrite -> X in *. rewrite -> Y in *. rewrite -> H in *. assert (Z:=Qplus_le_compat _ _ _ _ (x_ ((1#2)*d)%Qpos) (y_ ((1#2)*d)%Qpos)). simpl in Z. unfold Cap_raw in Z; simpl in Z. autorewrite with QposElim in Z. rewrite -> Qle_minus_iff in Z. ring_simplify in Z. rewrite -> Qle_minus_iff. ring_simplify. assumption. assert (0 < proj1_sig c) as cpos. { destruct c; exact q. } elim (Qlt_not_le _ _ cpos). rewrite -> X in *. rewrite -> Y in *. rewrite -> H in *. assert (Z:=Qplus_le_compat _ _ _ _ (x_ ((1#2)*d)%Qpos) (y_ ((1#2)*d)%Qpos)). simpl in Z. unfold Cap_raw in Z; simpl in Z. autorewrite with QposElim in Z. rewrite -> Qle_minus_iff in Z. ring_simplify in Z. rewrite -> Qle_minus_iff. ring_simplify. assumption. change (CRinv_pos c x== (CRinv_pos d y))%CR. rewrite -> H in *. rewrite -> Y in *. destruct (Qle_total (proj1_sig c) (proj1_sig d)); [|symmetry]; apply CRinv_pos_weaken; try assumption. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.model.lattice.CRlattice CoRN.model.totalorder.QMinMax Coq.QArith.Qabs CoRN.model.metric2.Qmetric CoRN.metric2.ProductMetric MathClasses.interfaces.canonical_names