proposition: Theorem lowest_i_such_that_ri_lt_r₀ : ∀ f L r n, r = nth_r 0 f L → (nth_r n f L < r)%nat → ∃ i, i ≤ n ∧ (i = O ∨ r ≤ nth_r (pred i) f L) ∧ (nth_r i f L < r)%nat.
proof: Proof. intros f L r n Hr Hrnr. subst r. revert f L Hrnr. induction n; intros. exfalso; revert Hrnr; apply Nat.lt_irrefl. destruct (lt_dec (nth_r n f L) (nth_r 0 f L)) as [H| H]. apply IHn in H. destruct H as (i, (Hin, (Hir, Hri))). exists i. split; [ idtac | split; assumption ]. apply Nat.le_le_succ_r; assumption. apply Nat.nlt_ge in H. exists (S n). split; [ reflexivity | idtac ]. split; [ idtac | assumption ]. right; rewrite Nat.pred_succ; assumption. Qed.
imports: Utf8 QArith NPeano Sorting Misc SlopeMisc Slope_base QbarM NbarM Field2 Fpolynomial Fsummation Newton ConvexHullMisc ConvexHull PolyConvexHull NotInSegment Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial Puiseux_base AlgCloCharPol CharactPolyn F1Eq PosOrder F1Prop InK1m Q_field RootHeadTail