proposition: Theorem psi_c₁_ne_0 : ∀ f L c₁ r Ψ, newton_segments f = Some L → r = root_multiplicity acf c₁ (Φq f L) → Ψ = quotient_phi_x_sub_c_pow_r (Φq f L) c₁ r → (apply_poly Ψ c₁ ≠ 0)%K.
proof: Proof. intros f L c r Ψ HL Hr HΨ. remember (Φq f L) as phi eqn:Hphi . subst Ψ; simpl. unfold apply_poly; simpl. unfold root_multiplicity in Hr. remember (al phi) as la eqn:Hla . subst phi; rewrite al_Φq in Hla. symmetry in Hr. eapply list_div_x_sub_c_ne_0; [ idtac | eassumption | reflexivity ]. rewrite Hla; intros H. simpl in H. rewrite Nat.sub_diag in H; simpl in H. apply lap_eq_cons_nil_inv in H. destruct H as (H, _). remember (ini_pt L) as jj eqn:Hj . destruct jj as (jq, αj); simpl. remember HL as HH; clear HeqHH. apply exists_ini_pt_nat in HH. destruct HH as (j, (x, Hx)). rewrite <- Hj in Hx; injection Hx; clear Hx; intros; subst jq x. simpl in H. revert H. eapply ord_coeff_non_zero_in_newt_segm; [ eassumption | idtac | idtac ]. symmetry in Hj. left; eassumption. rewrite nat_num_Qnat; reflexivity. Qed.
imports: Utf8 QArith NPeano ArithRing Misc Field2 ConvexHull Newton Fsummation Fpolynomial Puiseux_base Puiseux_series CharactPolyn