proposition: Theorem zerop_1st_n_const_coeff_false_iff : ∀ f L n, zerop_1st_n_const_coeff n f L = false ↔ ∀ i : nat, i ≤ n → (ps_poly_nth 0 (nth_pol i f L) ≠ 0)%ps.
proof: Proof. intros f L n. split; intros H. intros i Hin. revert f L i H Hin. induction n; intros. simpl in H. apply Nat.le_0_r in Hin; subst i. destruct (ps_zerop K (ps_poly_nth 0 f)); auto. discriminate H. simpl in H. destruct (ps_zerop K (ps_poly_nth 0 f)) as [H₁| H₁]. discriminate H. destruct i; auto; simpl. apply IHn; auto. apply Nat.succ_le_mono; assumption. revert f L H. induction n; intros; simpl. destruct (ps_zerop K (ps_poly_nth 0 f)) as [H₁| H₁]; auto. pose proof (H O (Nat.le_refl 0)) as H₂. contradiction. destruct (ps_zerop K (ps_poly_nth 0 f)) as [H₁| H₁]. pose proof (H O (Nat.le_0_l (S n))) as H₂. contradiction. apply IHn; intros i Hin. apply Nat.succ_le_mono, H in Hin; 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