proposition: Lemma lt_Succ_le_2 (alpha beta: E0): alpha o< E0_succ beta -> alpha o<= beta.
proof: Proof. destruct alpha, beta; cbn; intros. red in H; red; rewrite Le_iff. cbn; apply LT_succ_LE_2; 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)