proposition: Lemma subsequence_helper {u v : Rseq} (f : nat -> nat) : (forall n, f n < f (1 + n))%nat -> (forall n, u n = v (f n)) -> subsequence u v.
proof: Proof. intros Hf. hnf. unfold extractor. exists (exist is_extractor f Hf). eauto. Qed.
imports: Reals Rsequence_def Rsequence_facts Lia Lra