proposition: Lemma Feval_formula_compat env b f : hold b (Feval_PFormula env b f) <-> eval_formula add mul sub opp eqProp le lt F_of_Q id exp env f.
proof: Proof. by case: f => lhs op rhs; case: b => //=; 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)