proposition: Lemma Rseq_extractor_partition : forall phi, is_extractor phi -> forall n, phi 0 <= n -> exists p, phi p <= n < phi (S p).
proof: Proof. intros phi ephi. induction n. exists 0. split. assumption. apply (Rsubseq_n_le_extractor_n _ 1 ephi). destruct (le_le_S_dec (phi 0) n). intros _. destruct (IHn l) as [p [Hpn Hnsp]]. destruct (Compare.le_decide _ _ Hnsp). exists p. split; [constructor|]; assumption. exists (S p). rewrite e. intuition. intro l'; rewrite (Nat.le_antisymm _ _ l l'). exists 0. split. constructor. apply ephi. Qed.
imports: Reals Rsequence_def Rsequence_facts Lia Lra