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; auto. destruct (comparable_comp_spec a a0); (now subst || constructor; auto). - destruct (comparable_comp_spec b b0); (now subst || constructor; auto). Qed.
imports: Coq(Arith Compare_dec Lia Relation_Operators RelationClasses Disjoint_Union) hydras(ON_Generic MoreOrders)