proposition: Lemma CRinvT_pos_inv : forall (c:Qpos) (x:CR) x_, ('proj1_sig c <= x -> CRinv_pos c x == CRinvT x x_)%CR.
proof: Proof. intros c x [[e He]|[e He]] H. assert (X:(' proj1_sig e <= -x)%CR). rewrite <- (doubleSpeed_Eq x). intros d. eapply Qle_trans. apply He. simpl. do 2 (unfold Cap_raw;simpl). ring_simplify. apply Qle_refl. assert (' proj1_sig c <= ' (- proj1_sig e)%Q)%CR. eapply CRle_trans. apply H. intros d. eapply Qle_trans. apply X. simpl. do 2 (unfold Cap_raw;simpl). rewrite -> Qle_minus_iff. ring_simplify. apply Qle_refl. assert (0 < proj1_sig c) as cpos. { destruct c; exact q. } elim (Qlt_not_le _ _ cpos). assert (Y:=H0 (e)%Qpos). simpl in Y. do 2 (unfold Cap_raw in Y ;simpl in Y). rewrite -> Qle_minus_iff in Y. ring_simplify in Y. rewrite -> Qle_minus_iff. ring_simplify;assumption. assert (' proj1_sig e <= x)%CR. rewrite <- (doubleSpeed_Eq x). intros d. eapply Qle_trans. apply He. simpl. do 2 (unfold Cap_raw;simpl). ring_simplify. apply Qle_refl. destruct (Qle_total (proj1_sig c) (proj1_sig e)); [|symmetry]; apply CRinv_pos_weaken; 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