proposition: Lemma Rseq_equiv_subseq_compat : forall phi, Un ~ Vn -> (Un ⋅ phi) ~ (Vn ⋅ phi).
proof: Proof. intros [phi Hphi] Heq. intros eps Heps. destruct (Heq eps Heps) as [N HN]. exists N. intros n Hn; unfold Rseq_minus. apply HN. apply Nat.le_trans with (phi N). apply Rsubseq_n_le_extractor_n; assumption. apply nat_seq_growing_trans;auto with *. Qed.
imports: Reals Rsequence_def Rsequence_facts Lia Lra