fact: Definition check (lpe:list PEZ) (qe:PEZ) (certif: list (list PEZ) * list PEZ) := let (lla, lq) := certif in let lp := List.map norm lpe in PolZeq (norm qe) (mult_l lq (compute_list lla lp)).
imports: List Setoid BinPos BinList Znumtheory Morphisms Setoid Bool Algebra_syntax Ncring Ncring_initial Ncring_tac Integral_domain ZArith Lia