fact: Definition eval_op2 (o : Op2) : R -> R -> Prop := match o with | OpEq => req | OpNEq => fun x y : R => x ~= y | OpLe => rle | OpGe => fun x y : R => y <= x | OpLt => fun x y : R => x < y | OpGt => fun x y : R => y < x end.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl