proposition: Theorem ps_zero_in_K_1_m : ∀ m, in_K_1_m 0 m.
proof: Proof. intros m. constructor. exists (mkps 0 0 m). split; [ idtac | reflexivity ]. symmetry. rewrite ps_adjust_eq with (n := O) (k := m). unfold adjust_ps; simpl. rewrite series_shift_0; simpl. rewrite series_stretch_series_0. reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fpolynomial Newton Power_series Puiseux_series Ps_add Ps_mul Ps_div Ps_add_compat PSpolynomial Puiseux_base AlgCloCharPol PosOrder CharactPolyn ConvexHull PolyConvexHull F1Eq QbarM