proposition: Lemma cmp_eq x y : cmp x y = Eq -> x = y.
proof: Proof. destruct x; destruct y; simpl; try (refl||discr). intro e. apply Ty_CmpTransLeibniz.cmp_eq in e. subst. refl. Qed.
imports: CoLoR(LogicUtil OrdUtil LSimple RelUtil) Coq(Structures.Equalities Lia) Coq(Compare_dec)