proposition: Lemma Rseq_big_O_subseq_compat : forall phi, Un = O (Vn) -> (Un ⋅ phi) = O(Vn ⋅ phi).
proof: Proof. intros phi Heq. destruct Heq as [N [HN [N0 HN0]]]. exists N; split. assumption. exists N0; intros n Hn. apply HN0. apply Nat.le_trans with n. assumption. apply Rsubseq_n_le_extractor_n; destruct phi; assumption. Qed.
imports: Reals Rsequence_def Rsequence_facts Lia Lra