proposition: Lemma compare_correct alpha beta : CompSpec eq lt alpha beta (compare alpha beta).
proof: Proof. generalize (compare_reflect alpha beta); destruct (compare alpha beta); now constructor. Qed.
imports: Coq(Arith Compare_dec Lia Relation_Operators RelationClasses) hydras(Comparable Simple_LexProd ON_Generic)