proposition: Theorem root_formula : ∀ la c, (apply_lap la c = 0)%K → (la = [(- c)%K; 1%K … []] * lap_div_deg_1 la c)%lap.
proof: Proof. intros la c Hc. unfold lap_div_deg_1. remember (lap_mod_div_deg_1 R la c) as md eqn:Hmd . symmetry in Hmd. destruct md as [| r d]. rewrite lap_mul_nil_r. destruct la as [| a]; [ reflexivity | discriminate Hmd ]. destruct la as [| a]; [ discriminate Hmd | simpl ]. simpl in Hmd. simpl in Hc. injection Hmd; clear Hmd; intros Hd Hr. subst d; clear r Hr. rename a into a₀. apply list_nth_lap_eq; intros i. destruct i. simpl. rewrite summation_only_one. destruct la as [| a₁]. simpl. rewrite rng_mul_0_r. simpl in Hc. rewrite rng_mul_0_l, rng_add_0_l in Hc; assumption. simpl in Hc; simpl. remember (apply_lap la c * c + a₁)%K as v eqn:Hv . rewrite rng_mul_comm in Hc. apply rng_add_compat_r with (c := (- c * v)%K) in Hc. rewrite rng_add_0_l in Hc. rewrite rng_add_comm, rng_add_assoc in Hc. rewrite rng_mul_opp_l in Hc. rewrite rng_add_opp_l in Hc. rewrite rng_add_0_l in Hc. rewrite rng_mul_opp_l. assumption. rewrite nth_mul_deg_1; simpl. clear a₀ Hc. do 2 rewrite list_nth_mod_div_deg_1. revert i. induction la as [| a]; intros; simpl. rewrite match_id, list_skipn_nil; simpl. rewrite rng_mul_0_r, rng_add_0_l; reflexivity. destruct i; [ simpl | apply IHla ]. rewrite rng_add_assoc. rewrite rng_mul_opp_l, rng_mul_comm. rewrite rng_add_opp_l, rng_add_0_l; reflexivity. Qed.
imports: Utf8 QArith NPeano ArithRing Misc Field2 ConvexHull Newton Fsummation Fpolynomial Puiseux_base Puiseux_series CharactPolyn