proposition: Theorem Ψ_length : ∀ f L j k αj αk c₁ r Ψ, newton_segments f = Some L → ini_pt L = (Qnat j, αj) → fin_pt L = (Qnat k, αk) → r = root_multiplicity acf c₁ (Φq f L) → Ψ = quotient_phi_x_sub_c_pow_r (Φq f L) c₁ r → length (al Ψ) = (S (k - j) - r)%nat.
proof: Proof. intros f L j k αj αk c₁ r Ψ HL Hini Hfin Hr HΨ. subst Ψ. remember S as s; simpl. rewrite Hini; simpl. rewrite nat_num_Qnat; simpl. rewrite Nat.sub_diag; simpl. rewrite fold_char_pol with (αj := αj). rewrite <- Hini. rewrite length_list_quotient_phi_x_sub_c_pow_r. erewrite length_char_pol; try eassumption; try reflexivity. subst s; reflexivity. Qed.
imports: Utf8 QArith NPeano Sorted ConvexHullMisc ConvexHull PolyConvexHull Field2 Misc Newton NbarM QbarM SplitList Fsummation Fpolynomial Power_series Puiseux_series Ps_add Ps_mul Ps_div Ps_add_compat PSpolynomial Puiseux_base CharactPolyn AlgCloCharPol