proposition: Lemma NearBy_comp l1 l2 : l1 = l2 → ∀ ε1 ε2, QposEq ε1 ε2 → ∀ s, (NearBy l1 ε1 s ↔ NearBy l2 ε2 s).
proof: Proof. revert l1 l2. cut (∀ l1 l2 : X, l1 = l2 → ∀ ε1 ε2 : Qpos, QposEq ε1 ε2 → ∀ s : Stream X, NearBy l1 ε1 s → NearBy l2 ε2 s). intros. split. firstorder. intros. eapply H. symmetry. apply H0. unfold QposEq; symmetry. apply H1. assumption. unfold NearBy; simpl. intros l1 l2 Hl ε1 ε2 Hε. cofix F. intros s [H0 H]. constructor. apply (ball_wd X Hε _ _ (reflexivity _) _ _ Hl). 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