proposition: Lemma lt_eq_lt_dec alpha beta : {alpha o< beta} + {alpha = beta} + {beta o< alpha}.
proof: Proof. generalize (compare_reflect alpha beta). case_eq (ON_compare alpha beta). - intros; left; now right. - intros; left; now left. - intros; now right. Defined.
imports: Coq(Arith Compare_dec Lia) hydras(Simple_LexProd ON_Generic ON_mult ON_Omega Compat815)