proposition: Lemma compare x y : Compare lt eq x y.
proof: Proof. case_eq (cmp x y); intro h. apply EQ. apply cmp_eq. hyp. apply LT. hyp. apply GT. unfold lt. rewrite cmp_opp, h. refl. Qed.
imports: CoLoR(LogicUtil RelUtil SN EqUtil)