fact: Definition Reval_PFormula (e : PolEnv R) k (ff : Formula Z) : rtyp k := let eval := PEeval add mul sub opp R_of_Z id exp e in let (lhs,o,rhs) := ff in Reval_op2 k o (eval lhs) (eval rhs).
imports: elpi(elpi) Coq(QArith Ring) Coq.micromega(RingMicromega QMicromega EnvRing Tauto Lqa) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify) mathcomp.algebra_tactics(common)