proposition: Theorem eq_1_0_ps_0 : (1 = 0)%K → ∀ a, (a = 0)%ps.
proof: Proof. intros H a. apply order_inf. unfold order. remember (series_order (ps_terms a) 0) as v eqn:Hv . symmetry in Hv. destruct v as [v| ]; auto. apply series_order_iff in Hv. destruct Hv as (_, Hv). exfalso; apply Hv; simpl. apply eq_1_0_all_0; 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