proposition: Theorem list_root_mul_power_quotient : ∀ la c r len, list_root_multiplicity acf c la len = r → (la = [(- c)%K; 1%K … []] ^ r * list_quotient_phi_x_sub_c_pow_r R la c r)%lap.
proof: Proof. intros la c r len Hmult. revert la len Hmult. induction r; intros; simpl. rewrite lap_mul_1_l; reflexivity. rewrite <- lap_mul_assoc. eapply list_root_mult_succ_if in Hmult; [ idtac | reflexivity ]. destruct Hmult as (_, (Hz, Hmult)). rewrite <- IHr; [ idtac | eassumption ]. apply root_formula. apply lap_mod_deg_1_apply. unfold ac_is_zero in Hz. destruct (fld_zerop (lap_mod_deg_1 la c)) as [H| H]. rewrite H; reflexivity. contradiction. Qed.
imports: Utf8 QArith NPeano ArithRing Misc Field2 ConvexHull Newton Fsummation Fpolynomial Puiseux_base Puiseux_series CharactPolyn