proposition: Lemma o_dec : forall e1 e2 : A, {o e1 e2} + {~ o e1 e2}.
proof: Proof. unfold o. induction e1; induction e2. left; trivial. left; auto with arith. right; auto with arith. destruct (IHe1 e2); destruct IHe2; auto with arith. Defined.
imports: Coq(Setoid Relations Arith FunInd)