proposition: Lemma CRle_Qle : forall (x y:Q), (inject_Q_CR x <= inject_Q_CR y)%CR <-> (x <= y)%Q.
proof: Proof. split. intros H. destruct (Qlt_le_dec y x) as [X|X];[|assumption]. destruct (Qpos_sub _ _ X) as [c Hc]. assert (Y:=(H ((1#2)*c)%Qpos)). simpl in Y. unfold Cap_raw in Y; simpl in Y. rewrite -> Qle_minus_iff in Y. rewrite -> Hc in Y. autorewrite with QposElim in Y. ring_simplify in Y. elim (Qle_not_lt _ _ Y). rewrite -> Qlt_minus_iff. ring_simplify. apply Q.Qmult_lt_0_compat; auto with *. intros H e. simpl. unfold Cap_raw; simpl. rewrite -> Qle_minus_iff in H. apply Qle_trans with (0%Q);[|assumption]. rewrite -> Qle_minus_iff; ring_simplify. apply Qpos_nonneg. 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