proposition: Lemma compare_correct (alpha beta : E0) : CompSpec eq E0lt alpha beta (compare alpha beta).
proof: Proof. destruct alpha, beta; unfold compare, E0lt; cbn; destruct (T1.compare_correct cnf0 cnf1). - constructor 1; apply E0_eq_intro; subst; reflexivity. - constructor; now split. - constructor; split; auto. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles ArithRing Wellfounded Operators_Properties Logic.Eqdep_dec) hydras(Prelude.More_Arith Prelude.Restriction Prelude.DecPreOrder ON_Generic OrdNotations)