proposition: Lemma compare x y : Compare lt eq x y.
proof: Proof. apply EQ. destruct x; destruct y. refl. Qed.
imports: CoLoR(LogicUtil OrdUtil LSimple RelUtil) Coq(Structures.Equalities Lia) Coq(Compare_dec) CoLoR(VecUtil) CoLoR(LCompRewrite) CoLoR(SN LCall) CoLoR(EqUtil)