fact: Definition E0_pred (alpha: E0) : E0 := match Zero_Limit_Succ_dec alpha with inl _ => alpha | inr (exist _ beta _) => beta end.
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)