proposition: Theorem root_when_fin : ∀ f L n, zerop_1st_n_const_coeff (pred n) f L = false → zerop_1st_n_const_coeff n f L = true → (ps_pol_apply f (root_head 0 (pred n) f L) = 0)%ps.
proof: Proof. intros f L n Hnz Hz. destruct n. rewrite Nat.pred_0 in Hnz. rewrite Hnz in Hz; discriminate Hz. rewrite Nat.pred_succ in Hnz. rewrite Nat.pred_succ. remember Hnz as H; clear HeqH. eapply apply_nth_pol with (y := 0%ps) in H. rewrite rng_mul_0_r, rng_add_0_r in H; rewrite H. unfold ps_pol_apply, apply_poly. remember (S n) as sn. unfold apply_lap; simpl. remember (al (nth_pol sn f L)) as la eqn:Hla . symmetry in Hla. destruct la as [| a]; simpl. rewrite rng_mul_0_r; reflexivity. rewrite rng_mul_0_r, rng_add_0_l; subst sn. rewrite first_null_coeff with (a₁ := a); eauto . rewrite rng_mul_0_r; reflexivity. 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