proposition: Theorem f₁_root_f_root : ∀ f f₁ β γ c₁ y y₁, f₁ = next_pol f β γ c₁ → (y = ps_monom c₁ γ + ps_monom 1%K γ * y₁)%ps → (ps_pol_apply f₁ y₁ = 0)%ps → (ps_pol_apply f y = 0)%ps.
proof: Proof. intros f f₁ β γ c₁ y y₁ Hf₁ Hy Happ. destruct (ps_zerop K 1%ps) as [Hzo| Hnzo]. apply eq_1_0_all_0; assumption. subst f₁. unfold next_pol in Happ. unfold ps_pol_apply, apply_poly in Happ; simpl in Happ. unfold next_lap in Happ; simpl in Happ. unfold ps_pol_apply, apply_poly. rewrite apply_lap_mul in Happ. rewrite apply_lap_compose in Happ. simpl in Happ. rewrite ps_mul_0_l in Happ. do 2 rewrite ps_add_0_l in Happ. rewrite ps_add_comm, <- Hy in Happ. apply fld_eq_mul_0_r in Happ; [ assumption | apply ps_field | idtac ]. simpl; intros H. apply ps_monom_0_coeff_0 in H. apply Hnzo. unfold ps_one; rewrite H. apply ps_zero_monom_eq. 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