proposition: Lemma lt_Succ_inv : forall alpha beta, beta o< alpha <-> E0_succ beta o<= alpha.
proof: Proof. destruct alpha, beta; unfold lt, leq , E0_succ; cbn; split. - rewrite Le_iff. intro; now apply LT_succ_LE. - rewrite Le_iff. intro. now apply LT_succ_LE_R. 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)