proposition: Theorem cpol_degree_ge_1 : ∀ f L m, newton_segments f = Some L → pol_in_K_1_m f m → degree fld_zerop (Φq f L) ≥ 1.
proof: Proof. intros f L m HL Hm. remember (Pos.to_nat (q_of_m m (γ L))) as q eqn:Hq . remember (ini_pt L) as jj eqn:Hj . destruct jj as (jq, αj); simpl. remember HL as H; clear HeqH. apply exists_ini_pt_nat in H. destruct H as (j, (x, Hx)). rewrite <- Hj in Hx; injection Hx; clear Hx; intros; subst jq x. remember HL as Hk; clear HeqHk. apply exists_fin_pt_nat in Hk. destruct Hk as (k, (αk, Hk)). symmetry in Hk. remember HL as Hdeg; clear HeqHdeg. eapply phi_degree_is_k_sub_j_div_q in Hdeg; try eassumption. unfold has_degree in Hdeg. destruct Hdeg as (Hshr, (Hdeg, Hcnz)). remember HL as Hqkj; clear HeqHqkj. eapply q_is_factor_of_h_minus_j with (h := k) in Hqkj; try eassumption. destruct Hqkj as (n, Hqkj). destruct n. simpl in Hqkj. exfalso. remember HL as H; clear HeqH. apply j_lt_k with (j := j) (k := k) in H. apply Nat.sub_gt in H; contradiction. rewrite <- Hj; simpl. rewrite nat_num_Qnat; reflexivity. rewrite <- Hk; simpl. rewrite nat_num_Qnat; reflexivity. rewrite Hqkj in Hdeg, Hcnz. rewrite Nat.div_mul in Hdeg; [ idtac | subst q; apply Pos2Nat_ne_0 ]. rewrite Nat.div_mul in Hcnz; [ idtac | subst q; apply Pos2Nat_ne_0 ]. unfold pseudo_degree in Hdeg. unfold degree. remember (al (Φs q f L)) as la eqn:Hla . unfold Φs in Hla; simpl in Hla. rewrite Nat.sub_diag in Hla; simpl in Hla. rewrite <- Hj in Hla; simpl in Hla. rewrite nat_num_Qnat in Hla; simpl. rewrite Nat.sub_diag, list_pad_0. rewrite <- Hj; unfold fst. rewrite nat_num_Qnat. remember (order_coeff (List.nth j (al f) 0%ps)) as v eqn:Hv . remember (oth_pts L ++ [fin_pt L]) as pts eqn:Hpts . remember (List.map (term_of_point f) pts) as tl eqn:Htl . subst la; simpl. remember (make_char_pol R (S j) tl) as cf eqn:Hcf . remember (degree_plus_1_of_list fld_zerop cf) as d eqn:Hd . symmetry in Hd. destruct d; [ exfalso | apply le_n_S, Nat.le_0_l ]. subst cf. remember (Pos.to_nat (q_of_m m (γ L))) as nq. remember (make_char_pol R (S j) tl) as cf. pose proof (list_length_shrink_le nq [v … cf]) as Hlen. remember [v … cf] as vcf. rewrite Heqvcf in Hlen at 2. simpl in Hlen. subst vcf. apply degree_plus_1_is_0 in Hd. simpl in Hcnz. simpl in Hdeg. simpl in Hlen. apply le_S_n in Hlen. apply Hcnz. apply all_0_shrink_0; intros p. apply lap_eq_nil_nth; assumption. apply List.in_or_app; right; left; symmetry; eassumption. Qed.
imports: Utf8 QArith NPeano ArithRing Misc Field2 ConvexHull Newton Fsummation Fpolynomial Puiseux_base Puiseux_series CharactPolyn