proposition: Lemma compare_correct {a} (alpha beta : t a) : CompSpec eq lt alpha beta (compare alpha beta).
proof: Proof. unfold CompSpec, compare. - destruct alpha, beta; unfold compare,compare_O; cbn. case_eq (compare x x0); unfold lt; cbn. + constructor 1. destruct (comparable_comp_spec x x0); try discriminate. subst; f_equal; apply eq_proofs_unicity_on; decide equality. + constructor 2. destruct (comparable_comp_spec x x0); trivial; try discriminate. + constructor 3; destruct (comparable_comp_spec x x0); trivial; discriminate. Qed.
imports: Coq(Arith Relations Lia Logic.Eqdep_dec Ensembles Wellfounded.Inverse_Image Wellfounded.Inclusion RelationClasses) hydras(ON_Generic)