proposition: Theorem shrinkable_if : ∀ f q pt₁ pts, Sorted nat_fst_lt [pt₁ … pts] → q ≠ O → List.Forall (λ pt, (q | nat_num (fst pt) - nat_num (fst pt₁))%nat) pts → poly_shrinkable q POL (make_char_pol R (nat_num (fst pt₁)) (List.map (term_of_point f) [pt₁ … pts]))%pol.
proof: Proof. intros f q pt₁ pts Hsort Hq Hpts; simpl. rewrite Nat.sub_diag, list_pad_0. rewrite List.Forall_forall in Hpts. unfold poly_shrinkable; intros n Hn; simpl. destruct n. rewrite Nat.mod_0_l in Hn; auto with Arith. exfalso; apply Hn; reflexivity. revert n pt₁ Hsort Hpts Hn. induction pts as [| pt₂]; intros; [ destruct n; reflexivity | simpl ]. apply Sorted_inv in Hsort. destruct Hsort as (Hsort, Hrel). apply HdRel_inv in Hrel. unfold nat_fst_lt in Hrel; simpl in Hrel. destruct (lt_dec (nat_num (fst pt₁)) (nat_num (fst pt₂))) as [H₁| H₁]. unfold lt in H₁. remember (nat_num (fst pt₁)) as j eqn:Hj . remember (nat_num (fst pt₂)) as h eqn:Hh . destruct (eq_nat_dec (S j) h) as [H₂| H₂]. assert (pt₂ ∈ [pt₂ … pts]) as H by (left; auto). apply Hpts in H. rewrite <- Hh in H. rewrite <- H₂ in H. rewrite Nat_sub_succ_diag in H. destruct H as (c, Hc). symmetry in Hc. apply Nat.mul_eq_1 in Hc. destruct Hc as (Hc, Hq₁). rewrite Hq₁ in Hn. exfalso; apply Hn. reflexivity. destruct (lt_dec n (h - S j)) as [H₃| H₃]. rewrite list_nth_pad_lt; auto with Arith. apply Nat.nlt_ge in H₃. rewrite list_nth_pad_sub; auto with Arith. destruct (eq_nat_dec (h - S j) n) as [H₄| H₄]. exfalso. assert (pt₂ ∈ [pt₂ … pts]) as H by (left; auto). apply Hpts in H. rewrite <- Hh in H. destruct H as (c, Hc). rewrite <- H₄ in Hn. simpl in Hsort; simpl. rewrite <- Nat.sub_succ_l in Hn; auto with Arith. rewrite Nat.sub_succ in Hn. rewrite Hc in Hn. apply Hn, Nat.mod_mul; auto with Arith. remember (n - (h - S j))%nat as nhj eqn:Hnhj . symmetry in Hnhj. destruct nhj. apply Nat.sub_0_le in Hnhj. apply Nat_le_neq_lt in H₃; auto with Arith. apply Nat.nle_gt in H₃. contradiction. destruct (eq_nat_dec (S nhj mod q) 0) as [H₅| H₅]. apply Nat.mod_divides in H₅; auto with Arith. destruct H₅ as (c, Hc). apply Nat.add_sub_eq_nz in Hnhj; [ idtac | intros H; discriminate H ]. exfalso; apply Hn. rewrite <- Hnhj. rewrite Hc. rewrite <- Nat.add_succ_l. rewrite <- Nat.sub_succ_l; auto with Arith. rewrite Nat.sub_succ. assert (pt₂ ∈ [pt₂ … pts]) as H by (left; auto). apply Hpts in H. rewrite <- Hh in H. destruct H as (d, Hd). rewrite Nat.mul_comm. rewrite Hd, <- Nat.mul_add_distr_r. apply Nat.mod_mul; auto with Arith. rewrite Hh. apply IHpts; auto with Arith. intros pt Hpt. assert (pt ∈ [pt₂ … pts]) as H by (right; auto). apply Hpts in H. destruct H as (c, Hc). rewrite <- Hh. unfold divide. assert (pt₂ ∈ [pt₂ … pts]) as H by (left; auto). apply Hpts in H. rewrite <- Hh in H. destruct H as (d, Hd). exists (c - d)%nat. rewrite Nat.mul_sub_distr_r. rewrite <- Hc, <- Hd. rewrite Nat_sub_sub_distr; [ idtac | apply Nat.lt_le_incl; auto ]. rewrite Nat.sub_add; auto with Arith. apply Nat.lt_le_incl. eapply Nat.lt_trans; eauto with Arith. revert Hsort Hh Hpt; clear; intros; subst h. revert pt₂ pt Hsort Hpt. induction pts as [| pt₃]; intros; [ contradiction | idtac ]. destruct Hpt as [Hpt| Hpt]. subst pt. apply Sorted_inv in Hsort. destruct Hsort as (_, Hrel). apply HdRel_inv in Hrel. assumption. apply IHpts; auto with Arith. eapply Sorted_minus_2nd; eauto with Arith. intros x y z H₁ H₂; eapply Nat.lt_trans; eassumption. contradiction. Qed.
imports: Utf8 QArith Sorted NPeano ConvexHull ConvexHullMisc Misc NbarM QbarM Newton PolyConvexHull Field2 Fpolynomial PSpolynomial Puiseux_base Power_series Puiseux_series Ps_div Slope_base