proposition: Theorem a₀_0_root_0 : ∀ f, (ps_poly_nth 0 f = 0)%ps → (ps_pol_apply f 0 = 0)%ps.
proof: Proof. intros f H. unfold ps_pol_apply, apply_poly, apply_lap; simpl. unfold ps_poly_nth in H. destruct (al f) as [| a la]; [ reflexivity | simpl ]. unfold ps_lap_nth in H; simpl in H. rewrite rng_mul_0_r, rng_add_0_l; assumption. 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