proposition: Theorem multiplicity_not_decreasing : ∀ f L r, (∀ i : nat, if multiplicity_decreases f L i then False else True) → root_multiplicity acf (ac_root (Φq f L)) (Φq f L) = r → ∀ j, r ≤ nth_r j f L.
proof: Proof. intros f L r Hn Hr j. pose proof Hn j as H. remember (multiplicity_decreases f L j) as p eqn:Hp . destruct p as [| p]; [ contradiction | ]. unfold multiplicity_decreases in Hp; simpl in Hp. destruct (lt_dec (root_multiplicity acf (nth_c j f L) (Φq (nth_pol j f L) (nth_ns j f L))) (root_multiplicity acf (ac_root (Φq f L)) (Φq f L))) as [| H₁]. contradiction . clear Hp. apply Nat.nlt_ge in H₁. rewrite Hr in H₁. erewrite <- nth_r_n in H₁; try eassumption; reflexivity. 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 RootAnyR