proposition: Lemma CRle_antisym : forall x y, (x==y <-> (x <= y /\ y <= x))%CR.
proof: Proof. intros x y. split;[intros H;rewrite -> H;split; apply CRle_refl|]. intros [H1 H2]. rewrite <- (doubleSpeed_Eq x). rewrite <- (doubleSpeed_Eq y). apply regFunEq_equiv, regFunEq_e. intros e. apply ball_weak. apply Qpos_nonneg. split;[apply H2|]. specialize (H1 e). apply Qopp_le_compat in H1. rewrite Qopp_involutive in H1. refine (Qle_trans _ _ _ _ H1). simpl. unfold Cap_raw. simpl. ring_simplify. apply Qle_refl. Qed.
imports: QArith Qabs CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.model.metric2.CRmetric CoRN.model.totalorder.QMinMax CoRN.model.metric2.Qmetric CoRN.metric2.ProductMetric CoRN.stdlib_omissions.Pair MathClasses.interfaces.canonical_names