fact: Definition Qeval_bop2 (o : Op2) : Q -> Q -> bool := match o with | OpEq => Qeq_bool | OpNEq => fun x y => negb (Qeq_bool x y) | OpLe => Qle_bool | OpGe => fun x y => Qle_bool y x | OpLt => Qlt_bool | OpGt => fun x y => Qlt_bool y x end.
imports: OrderedRing RingMicromega Refl QArith Qfield EnvRing