proposition: Theorem lap_add_cons : ∀ α (R : ring α) a b la lb, ([a … la] + [b … lb] = [(a + b)%K … la + lb])%lap.
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