proposition: Lemma pop2_bop2 (op : Op2) (q1 q2 : R) : Reval_bop2 op q1 q2 <-> Reval_pop2 op q1 q2.
proof: Proof. by case: op => //=; rewrite eqPropE eqBoolE; split => /eqP. 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)