proposition: Theorem root_multiplicity_0 : ∀ c cf, c = ac_root cf → root_multiplicity acf c cf = 0%nat → (degree fld_zerop cf = 0)%nat.
proof: Proof. intros c cf Hc Hr. unfold root_multiplicity in Hr. unfold degree, apply_poly. remember (al cf) as la. symmetry in Heqla. destruct la as [| a]; [ reflexivity | simpl ]. simpl in Hr. unfold lap_mod_deg_1 in Hr; simpl in Hr. destruct (fld_zerop (apply_lap la c * c + a)%K) as [H₁| H₁]. discriminate Hr. remember (degree fld_zerop cf) as deg eqn:Hdeg . symmetry in Hdeg. destruct deg. unfold degree in Hdeg. rewrite Heqla in Hdeg. simpl in Hdeg. assumption. assert (degree fld_zerop cf ≥ 1)%nat as H. rewrite Hdeg; apply le_n_S, Nat.le_0_l. clear Hdeg. apply ac_prop_root in H. rewrite <- Hc in H. unfold apply_poly in H. rewrite Heqla in H; simpl in H. contradiction. 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