proposition: Lemma compare_reflect {a:A} (alpha beta : t a) : match (compare alpha beta) with Datatypes.Lt => lt alpha beta | Eq => alpha = beta | Gt => lt beta alpha end.
proof: Proof. now destruct (compare_correct alpha beta). Qed.
imports: Coq(Arith Relations Lia Logic.Eqdep_dec Ensembles Wellfounded.Inverse_Image Wellfounded.Inclusion RelationClasses) hydras(ON_Generic)