proposition: Theorem k_le_r : ∀ αj₁ αk₁ k₁ r pt pts v ms pts₁ pts₂, pts = pts₁ ++ [fin_pt ms … pts₂] → Sorted fst_lt [(Qnat 0, αj₁); pt … pts] → ms = minimise_slope (Qnat 0, αj₁) pt pts → fin_pt ms = (Qnat k₁, αk₁) → v == 0 → 0 < αj₁ → 0 <= αk₁ → (Qnat (S r), v) ∈ [pt … pts₁] → k₁ ≤ S r.
proof: Proof. intros αj₁ αk₁ k₁ r pt pts v ms pts₁ pts₂. intros Hpts Hsort Heqms Hfin₁ Hz Hpos₀ Hnnegk Hsr. apply Nat.nlt_ge. intros Hrk. assert (slope ms < slope_expr (Qnat (S r), v) (Qnat k₁, αk₁)) as H. apply Qnot_le_lt. intros H. rewrite slope_slope_expr in H; [ | symmetry; eassumption ]. rewrite <- Hfin₁ in H. rewrite Hfin₁ in H; simpl in H. unfold slope_expr in H; simpl in H. rewrite Hz in H. rewrite Q_sub_0_r in H. unfold Qle in H; simpl in H. rewrite Qnum_inv_Qnat_sub in H; [ | assumption ]. rewrite Z.mul_1_r in H. remember Hrk as Hk₁; clear HeqHk₁. apply Nat.lt_trans with (n := O) in Hk₁; [ idtac | apply Nat.lt_0_succ ]. rewrite Qnum_inv_Qnat_sub in H; [ idtac | assumption ]. rewrite Z.mul_1_r in H. rewrite Qden_inv_Qnat_sub in H; [ idtac | assumption ]. rewrite Qden_inv_Qnat_sub in H; [ idtac | assumption ]. rewrite Nat.sub_0_r in H. rewrite Z.mul_opp_l in H. rewrite Z.add_opp_r in H. rewrite Z.mul_comm in H. rewrite Pos2Z.inj_mul in H. rewrite Pos2Z.inj_mul in H. rewrite Z.mul_comm in H. rewrite Pos2Z.inj_mul in H. rewrite Z.mul_comm in H. do 2 rewrite <- Z.mul_assoc in H. rewrite Z.mul_comm in H. rewrite Z.mul_assoc in H. rewrite Z.mul_assoc in H. remember (Zpos (Qden αj₁) * Zpos (Pos.of_nat k₁) * Qnum αk₁ * Zpos (Qden αk₁))%Z as x. rewrite Z.mul_shuffle0 in H. subst x. apply Z.mul_le_mono_pos_r in H; [ idtac | apply Pos2Z.is_pos ]. rewrite Z.mul_sub_distr_r in H. rewrite Nat2Pos.inj_sub in H; [ idtac | intros HH; discriminate HH ]. rewrite Pos2Z.inj_sub in H. rewrite Z.mul_sub_distr_l in H. rewrite <- Z.mul_assoc, Z.mul_comm in H. rewrite <- Z.mul_assoc, Z.mul_comm in H. apply Z.le_add_le_sub_r in H. apply Z.le_add_le_sub_r in H. apply Z.nlt_ge in H. apply H. rewrite <- Z.add_assoc. apply Z.lt_sub_lt_add_l. rewrite Z.sub_diag. apply Z.add_pos_nonneg. apply Z.mul_pos_pos. apply Z.mul_pos_pos; [ idtac | apply Pos2Z.is_pos ]. unfold Qlt in Hpos₀; simpl in Hpos₀. rewrite Z.mul_1_r in Hpos₀; assumption. rewrite <- Pos2Z.inj_sub; [ apply Pos2Z.is_pos | idtac ]. apply -> Pos.compare_lt_iff. rewrite <- Nat2Pos.inj_compare. apply nat_compare_lt; assumption. intros HH; discriminate HH. intros Hk; subst k₁. revert Hrk; apply Nat.nlt_0_r. apply Z.mul_nonneg_nonneg; [ | apply Pos2Z.is_nonneg ]. apply Z.mul_nonneg_nonneg; [ | apply Pos2Z.is_nonneg ]. unfold Qle in Hnnegk; simpl in Hnnegk. rewrite Z.mul_1_r in Hnnegk; assumption. apply -> Pos.compare_lt_iff. rewrite <- Nat2Pos.inj_compare. apply nat_compare_lt; assumption. intros HH; discriminate HH. intros Hk; subst k₁. revert Hrk; apply Nat.nlt_0_r. rename H into Hsl. subst pts. remember Heqms as H; clear HeqH. symmetry in H. destruct Hsr as [Hsr| Hsr]. subst pt. eapply minimise_slope_expr_le in H; try eassumption. apply Qle_not_lt in H; contradiction. simpl; apply Qnat_lt; assumption. eapply min_slope_le with (pt₃ := (Qnat (S r), v)) in H; try eassumption. apply Qle_not_lt in H; contradiction. apply List.in_or_app; left; assumption. simpl; apply Qnat_lt; 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