proposition: Theorem degree_eq_0_if : ∀ cf, degree fld_zerop cf = O → (cf = POL [])%pol ∨ (∃ a, (a ≠ 0)%K ∧ (cf = POL [a])%pol).
proof: Proof. intros cf Hdeg. unfold degree in Hdeg. unfold eq_poly; simpl. remember (al cf) as la; clear Heqla. induction la as [| a]; [ left; reflexivity | idtac ]. simpl in Hdeg. remember (degree_plus_1_of_list fld_zerop la) as deg eqn:Hdeg₁ . symmetry in Hdeg₁. destruct deg. clear Hdeg. pose proof (IHla (Nat.eq_refl O)) as H. clear IHla. destruct H as [Hla| Hla]. rewrite Hla. destruct (fld_zerop a) as [H₁| H₁]. left; rewrite H₁. apply lap_eq_0. right. exists a. split; [ assumption | idtac ]. rewrite Hla; reflexivity. clear cf. destruct Hla as (b, (Hb, Hla)). rewrite Hla. right. revert a b Hb Hla. induction la as [| c]; intros. apply lap_eq_nil_cons_inv in Hla. destruct Hla; contradiction. simpl in Hdeg₁. apply lap_eq_cons_inv in Hla. destruct Hla as (Hcb, Hla). remember (degree_plus_1_of_list fld_zerop la) as deg eqn:Hdeg . symmetry in Hdeg. destruct deg. destruct (fld_zerop c) as [H₁| H₁]; [ idtac | discriminate Hdeg₁ ]. rewrite H₁ in Hcb. symmetry in Hcb; contradiction. discriminate Hdeg₁. discriminate Hdeg. 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