proposition: Lemma Rseq_little_O_subseq_compat : forall phi, Un = o (Vn) -> (Un ⋅ phi) = o(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