proposition: Lemma lt_eq_lt_dec alpha beta : {lt alpha beta} + {alpha = beta} + {lt beta alpha}.
proof: Proof. generalize (compare_reflect alpha beta). destruct (compare alpha beta). - left;right; auto. - left;left; auto. - right; auto. Defined.
imports: Coq(Arith Compare_dec Lia Relation_Operators RelationClasses) hydras(Comparable Simple_LexProd ON_Generic)