proposition: Lemma Qle_closed : (forall e x, (forall d : Qpos, x <= e+ proj1_sig d) -> x <= e).
proof: Proof. intros. apply Qnot_lt_le. intro abs. assert (0 < (x - e) * (1#2)) as H0. { apply (Qle_lt_trans _ (0*(1#2))). discriminate. apply Qmult_lt_r. reflexivity. rewrite <- (Qplus_opp_r e). apply Qplus_lt_l. exact abs. } specialize (H (exist _ _ H0)). simpl in H. apply (Qplus_le_l _ _ (-x*(1#2))) in H. ring_simplify in H. apply Qmult_le_l in H. exact (Qle_not_lt _ _ H abs). reflexivity. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.Prelength CoRN.metric2.Classification CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax Coq.QArith.Qabs CoRN.metric2.UniformContinuity MathClasses.implementations.stdlib_rationals