fact: Fixpoint PCond' (l : seq R) (le : seq (PExpr C)) : P := match le with | [::] => ptrue | [:: e1] => pneg (req (eval l e1) rO) | e1 :: l1 => pand (pneg (req (eval l e1) rO)) (PCond' l l1) end.
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)