proposition: Lemma Qinv_pos_uc_wd : forall (c1 c2:Qpos), (proj1_sig c1 <= proj1_sig c2) -> forall x, (proj1_sig c2 <= x) -> msp_eq (Qinv_pos_uc c1 x) (Qinv_pos_uc c2 x).
proof: Proof. intros c1 c2 Hc x Hx. simpl. setoid_replace (Qmax (proj1_sig c2) x) with x by (rewrite <- Qle_max_r; assumption). setoid_replace (Qmax (proj1_sig c1) x) with x. apply Qball_Reflexive. discriminate. rewrite <- Qle_max_r. apply Qle_trans with (proj1_sig c2); 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