proposition: Lemma L1: leq lt gamma alpha.
proof: Proof. destruct (lt_eq_lt_dec gamma alpha) as [[Hlt | Heq] | Hgt]. - rewrite le_lt_eq; now left. - rewrite le_lt_eq; now right. - destruct Halphabeta. exfalso. eauto. Qed.
imports: hydras(OrdinalNotations.ON_Generic) Coq(Relations)