proposition: Lemma NearBy_weak l (ε1 ε2 : Qpos) : proj1_sig ε1 <= proj1_sig ε2 → ∀ s, NearBy l ε1 s → NearBy l ε2 s.
proof: Proof. unfold NearBy; simpl. cofix F. intros Hε s [H0 H]. constructor. eapply ball_weak_le. apply Hε. assumption. auto. Qed.
imports: CoRN.algebra.RSetoid CoRN.model.totalorder.QposMinMax Coq.QArith.QArith Coq.Bool.Bool CoRN.metric2.Complete MathClasses.theory.CoqStreams MathClasses.interfaces.abstract_algebra MathClasses.theory.streams MathClasses.orders.naturals