proposition: Lemma compare_reflect alpha beta : match (compare alpha beta) with Lt => lt alpha beta | Eq => alpha = beta | Gt => lt beta alpha end.
proof: Proof. destruct alpha, beta; cbn. unfold compare, compare_mult; cbn. destruct (comparable_comp_spec b b0). - subst; destruct (comparable_comp_spec a a0). + now subst. + now constructor 2. + now constructor 2. - now constructor 1. - now constructor 1. Qed.
imports: Coq(Arith Compare_dec Lia Relation_Operators RelationClasses) hydras(Comparable Simple_LexProd ON_Generic)