proposition: Lemma succb_not_lim alpha: is_successor alpha -> ~ is_limit alpha.
proof: Proof. induction alpha. - intro;apply zero_not_lim. - inversion_clear 1. + apply (F_not_lim (S n)). + red;inversion 1. * subst alpha3;inversion H1. * case IHalpha3;auto. Qed.
imports: Coq(Arith List Lia Compare_dec Relations Wellfounded RelationClasses) hydras(Epsilon0) hydras(More_Arith Restriction) hydras(ON_Generic) hydras(rpo.term rpo.rpo) hydras(T2) hydras(Compat815)