fact: Definition eval_op1 (o : Op1) : R -> Prop := match o with | Equal => fun x => x == 0 | NonEqual => fun x : R => x ~= 0 | Strict => fun x : R => 0 < x | NonStrict => fun x : R => 0 <= x end.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl