proposition: Theorem lowest_zerop_1st_n_const_coeff : ∀ f L n, zerop_1st_n_const_coeff n f L = true → ∃ i, i = lowest_with_zero_1st_const_coeff n f L ∧ i ≤ n ∧ (i = O ∨ zerop_1st_n_const_coeff (pred i) f L = false) ∧ zerop_1st_n_const_coeff i f L = true.
proof: Proof. intros f L n Hz. remember (lowest_with_zero_1st_const_coeff n f L) as i eqn:Hi. exists i; split; [ reflexivity | ]. revert f L i Hz Hi. induction n; intros. simpl in Hi; subst i. split; [ reflexivity | ]. split; [ left; reflexivity | assumption ]. simpl in Hi, Hz. remember (ps_zerop K (ps_poly_nth 0 f)) as t eqn:Ht . destruct t as [t| t]. subst i. split; [ apply Nat.le_0_l | ]. split; [ left; reflexivity | simpl; rewrite <- Ht; reflexivity ]. destruct i; [ discriminate Hi | ]. remember (ac_root (Φq f L)) as c eqn:Hc . remember (next_pol f (β L) (γ L) c) as f₁ eqn:Hf₁ ; subst c. remember (option_get phony_ns (newton_segments f₁)) as L₁ eqn:HL₁ . apply Nat.succ_inj in Hi. pose proof (IHn f₁ L₁ i Hz Hi) as H. destruct H as (Hin, (Hip, Hii)). split; [ rewrite <- Nat.succ_le_mono; assumption | simpl ]. destruct Hip as [Hip| Hip]. split; [ right; simpl | ]. subst i; simpl. rewrite Hip; simpl. rewrite <- Ht; reflexivity. rewrite <- Ht, <- Hf₁, <- HL₁; assumption. split; [ right; simpl | ]. destruct i; simpl; [ rewrite <- Ht; reflexivity | ]. rewrite <- Ht, <- Hf₁, <- HL₁; assumption. rewrite <- Ht, <- Hf₁, <- HL₁; 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