proposition: Theorem nth_r_n : ∀ f L f₁ L₁ c₁ n, f₁ = nth_pol n f L → L₁ = nth_ns n f L → c₁ = nth_c n f L → nth_r n f L = root_multiplicity acf c₁ (Φq f₁ L₁).
proof: Proof. intros f L f₁ L₁ c₁ n Hf₁ HL₁ Hc₁. revert f L f₁ L₁ c₁ Hf₁ HL₁ Hc₁. induction n; intros; [ subst; reflexivity | simpl ]. apply IHn; subst; reflexivity. Qed.
imports: Utf8 QArith NPeano Sorting Misc Field2 Fpolynomial Fsummation Newton ConvexHull Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial Puiseux_base AlgCloCharPol CharactPolyn F1Eq F1Prop Q_field PosOrder QbarM