proposition: Lemma CRinv_pos_Qinv : forall (c:Qpos) x, (proj1_sig c <= x)%Q -> (CRinv_pos c (' x) == (' (/x)))%CR.
proof: Proof. intros c x H. apply regFunEq_equiv, regFunEq_e. intros e. simpl. setoid_replace (Qmax (proj1_sig c) x) with x. apply Qball_Reflexive. apply (Qpos_nonneg (e+e)). rewrite <- Qle_max_r. 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