proposition: Theorem first_null_coeff : ∀ f₁ L₁ i a₁ la₁, zerop_1st_n_const_coeff i f₁ L₁ = false → zerop_1st_n_const_coeff (S i) f₁ L₁ = true → al (nth_pol (S i) f₁ L₁) = [a₁ … la₁] → (a₁ = 0)%ps.
proof: Proof. intros f₁ L₁ i a₁ la₁ Hnz₁ Hz₁ Hla₁. revert f₁ L₁ a₁ la₁ Hnz₁ Hz₁ Hla₁. induction i; intros. simpl in Hnz₁, Hz₁, Hla₁. destruct (ps_zerop K (ps_poly_nth 0 f₁)) as [H₁| H₁]. discriminate Hnz₁. remember (ac_root (Φq f₁ L₁)) as c₁ eqn:Hc₁ . remember (next_pol f₁ (β L₁) (γ L₁) c₁) as f₂ eqn:Hf₂ . remember (option_get phony_ns (newton_segments f₂)) as L₂ eqn:HL₂ . destruct (ps_zerop K (ps_poly_nth 0 f₂)) as [H₂| H₂]. unfold ps_poly_nth, ps_lap_nth in H₂; simpl in H₂. unfold next_pol in Hf₂. rewrite Hla₁ in Hf₂. rewrite Hf₂ in H₂; simpl in H₂. assumption. discriminate Hz₁. remember (S i) as si; simpl in Hz₁, Hla₁; subst si. simpl in Hnz₁. destruct (ps_zerop K (ps_poly_nth 0 f₁)) as [H₁| H₁]. discriminate Hnz₁. remember (ac_root (Φq f₁ L₁)) as c₁ eqn:Hc₁ . remember (next_pol f₁ (β L₁) (γ L₁) c₁) as f₂ eqn:Hf₂ . remember (option_get phony_ns (newton_segments f₂)) as L₂ eqn:HL₂ . eapply IHi; eauto . 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