proposition: Lemma ZLS_dec (alpha : t) : {alpha = 0} + {Limit alpha} + {beta : t | Successor alpha beta}.
proof: Proof. destruct alpha. - destruct n. + left; now left. + right; exists (inl n). split. * constructor. auto with arith. * intros beta Hbeta Hbeta'; inversion Hbeta; subst; inversion Hbeta';subst; try lia. - destruct n. left;right. split. + exists (inl 0); constructor. + inversion 1; subst. exists (inl (S x)); split; constructor;auto with arith. abstract lia. + right; exists (inr n); split. * constructor. auto with arith. * intros beta Hbeta Hbeta'; inversion Hbeta; subst; inversion Hbeta';subst; try lia. Defined.
imports: Coq(Arith Compare_dec Lia) hydras(Comparable Simple_LexProd ON_Generic ON_plus ON_Omega Compat815)