proposition: Lemma compare_correct (a b: t): CompSpec eq lt a b (compare a b).
proof: Proof. unfold lt; generalize (compare_reflect a b). destruct (compare a b); now constructor. Qed.
imports: hydras(T1 E0 Comparable) Coq(Arith Logic.Eqdep_dec Peano_dec List Bool Recdef Lia Wellfounded.Inverse_Image Wellfounded.Inclusion RelationClasses )