proposition: Lemma Rsubseq_n_le_extractor_n : forall phi n, is_extractor phi -> n <= phi n.
proof: Proof. intros phi n Hphi. induction n. apply Nat.le_0_l. eapply Nat.le_trans with (S (phi n)). apply (le_n_S _ _ IHn). apply Hphi. Qed.
imports: Reals Rsequence_def Rsequence_facts Lia Lra