fact: Fixpoint compute_list (lla: list (list PEZ)) (lp:list PolZ) := match lla with | List.nil => lp | la::lla => compute_list lla ((mult_l la lp)::lp) end.
imports: List Setoid BinPos BinList Znumtheory Morphisms Setoid Bool Algebra_syntax Ncring Ncring_initial Ncring_tac Integral_domain ZArith Lia