fact: Definition Qeval_op1 (o : Op1) : Q -> Prop := match o with | Equal => fun x : Q => x == 0 | NonEqual => fun x : Q => ~ x == 0 | Strict => fun x : Q => 0 < x | NonStrict => fun x : Q => 0 <= x end.
imports: OrderedRing RingMicromega Refl QArith Qfield EnvRing