proposition: Theorem char_pol_root_ne_0 : ∀ f L m c₁, newton_segments f = Some L → pol_in_K_1_m f m → c₁ = ac_root (Φq f L) → (c₁ ≠ 0)%K.
proof: Proof. intros f L m c₁ HL Hm Hc₁. remember HL as Happ; clear HeqHapp. eapply cpol_degree_ge_1 with (K := K) in Happ; eauto . apply ac_prop_root in Happ. rewrite <- Hc₁ in Happ. remember HL as Hini; clear HeqHini. apply exists_ini_pt_nat in Hini. destruct Hini as (j, (αj, Hini)). intros Hc; rewrite Hc in Happ. unfold apply_poly in Happ; simpl in Happ. rewrite Nat.sub_diag, list_pad_0 in Happ. simpl in Happ. rewrite rng_mul_0_r, rng_add_0_l in Happ. revert Happ. eapply ord_coeff_non_zero_in_newt_segm; eauto . rewrite Hini; left; simpl. rewrite nat_num_Qnat; reflexivity. Qed.
imports: Utf8 QArith NPeano Sorted Misc QbarM SplitList Field2 Fpolynomial Fsummation Newton ConvexHullMisc ConvexHull Puiseux_base Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial AlgCloCharPol CharactPolyn F1Eq PosOrder InK1m