fact: Fixpoint PEeval_list C R (R_of_C : C -> R) zero opp add sub one mul exp (l : seq R) (lpe : list (RExpr R * RExpr R * PExpr C * PExpr C)) : seq R := if lpe is (_, _, lhs, rhs) :: lpe then PEeval zero one add mul sub opp R_of_C id exp l lhs :: PEeval zero one add mul sub opp R_of_C id exp l rhs :: PEeval_list R_of_C zero opp add sub one mul exp l lpe else [::].
imports: elpi(elpi) Coq(ZArith Ring Ring_polynom Field_theory) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify) mathcomp.algebra_tactics(common)