proposition: Lemma Reval_formula_compat (env : PolEnv R) k (f : Formula Z) : hold k (Reval_PFormula env k f) <-> eval_formula add mul sub opp eqProp le lt R_of_Z id exp env f.
proof: Proof. by case: f => lhs op rhs; case: k => //=; rewrite pop2_bop2. Qed.
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)