proposition: Lemma compare_correct alpha beta : CompSpec eq ON_lt alpha beta (ON_compare alpha beta).
proof: Proof. generalize (compare_reflect alpha beta). destruct (ON_compare alpha beta); now constructor. Qed.
imports: Coq(Arith Compare_dec Lia) hydras(Simple_LexProd ON_Generic ON_mult ON_Omega Compat815)