proposition: Theorem degree_plus_1_is_0 : ∀ la, degree_plus_1_of_list fld_zerop la = 0%nat → lap_eq la [].
proof: Proof. intros la H. induction la as [| a]; [ reflexivity | idtac ]. simpl in H. remember (degree_plus_1_of_list fld_zerop la) as d eqn:Hd . symmetry in Hd. destruct d; [ idtac | discriminate H ]. constructor; [ idtac | apply IHla; reflexivity ]. destruct (fld_zerop a); [ assumption | discriminate H ]. Qed.
imports: Utf8 QArith NPeano ArithRing Misc Field2 ConvexHull Newton Fsummation Fpolynomial Puiseux_base Puiseux_series CharactPolyn