proposition: Lemma extractor_comp : forall phi1 phi2, is_extractor phi1 -> is_extractor phi2 -> is_extractor (fun n => phi1 (phi2 n)).
proof: Proof. intros phi1 phi2 H1 H2 n. apply nat_seq_strict_growing_trans; trivial. Qed.
imports: Reals Rsequence_def Rsequence_facts Lia Lra