proposition: Theorem fold_lap_inject_K_in_Kx : ∀ la, List.map (λ c : α, ps_monom c 0) la = lap_inject_K_in_Kx la.
proof: Proof. reflexivity. Qed.
imports: Utf8 QArith NPeano Sorted Misc QbarM SplitList Field2 Fpolynomial Fsummation Newton ConvexHullMisc ConvexHull Puiseux_base Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial AlgCloCharPol CharactPolyn F1Eq PosOrder InK1m