proposition: Lemma Succ_not_Zero alpha: E0is_succ alpha -> alpha <> E0zero.
proof: Proof. destruct alpha;unfold E0is_succ, E0zero; cbn. intros H H0; injection H0; intro;subst; discriminate H. 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)