proposition: Theorem multiplicity_lt_length : ∀ cf c, (al cf ≠ [])%lap → (root_multiplicity acf c cf < length (al cf))%nat.
proof: Proof. intros cf c Hnz. unfold root_multiplicity. remember (al cf) as la; clear Heqla. remember (length la) as len eqn:H. assert (length la ≤ len) as Hlen by (apply Nat.eq_le_incl, Nat.eq_sym, H). clear H. revert la Hnz Hlen. induction len; intros. apply Nat.le_0_r in Hlen. destruct la as [| a]; [ exfalso; apply Hnz; reflexivity | idtac ]. discriminate Hlen. simpl. destruct (fld_zerop (lap_mod_deg_1 la c)) as [H₁| H₁]. apply lt_n_S. destruct la as [| a]; [ exfalso; apply Hnz; reflexivity | idtac ]. simpl in Hlen. apply le_S_n in Hlen. unfold lap_mod_deg_1 in H₁; simpl in H₁. unfold lap_div_deg_1; simpl. apply IHlen. revert Hnz H₁; clear; intros. revert a c Hnz H₁. induction la as [| b]; intros. simpl in H₁. rewrite rng_mul_0_l, rng_add_0_l in H₁. exfalso; apply Hnz; rewrite H₁. constructor; reflexivity. simpl in H₁; simpl. intros H. apply lap_eq_cons_nil_inv in H. destruct H as (H₂, H₃). rewrite H₂ in H₁. rewrite rng_mul_0_l, rng_add_0_l in H₁. revert H₃. apply IHla with (a := b); [ | assumption ]. intros H. rewrite H in Hnz. apply Hnz; rewrite H₁. constructor; reflexivity. rewrite length_lap_mod_div_deg_1; assumption. apply Nat.lt_0_succ. Qed.
imports: Utf8 QArith NPeano Sorting Misc SlopeMisc Slope_base QbarM NbarM Field2 Fpolynomial Fsummation Newton ConvexHullMisc ConvexHull PolyConvexHull NotInSegment Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial Puiseux_base AlgCloCharPol CharactPolyn F1Eq PosOrder F1Prop InK1m Q_field RootHeadTail