fact: Definition Reval_pop2 (o : Op2) : R -> R -> Prop := match o with | OpEq => eqProp | OpNEq => fun x y => ~ eqProp x y | OpLe => le | OpGe => fun x y => le y x | OpLt => lt | OpGt => fun x y => lt y x end.
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)