proposition: Lemma succ_limit_dec : forall a, nf a -> {a = zero} +{is_successor a}+{is_limit a}.
proof: Proof. intro a;elim a. - left;left;auto. - intro alpha;case alpha;intro. + intro beta;case beta;intro. * intros; assert (t=zero). { inversion H2;auto. inversion H7;lt_clean. } subst t;left;right. constructor. * destruct n0;destruct t2. -- right;constructor; auto with T2. nf_inv. -- intros H1 H2;case H1. ++ nf_inv. ++ destruct 1. discriminate e. left;right. constructor;auto with T2. ++ right; constructor; auto. -- right; constructor;auto with T2. nf_inv. -- intros H1 H2;case H1. ++ nf_inv. ++ destruct 1. discriminate e. left;right;constructor. auto with T2. auto with T2. ++ right;constructor;auto with T2. + intros; case H1. * nf_inv. * destruct 1. -- subst t3;right;constructor;auto with T2. nf_inv. nf_inv. -- left;right;constructor;auto with T2. * right;constructor;auto with T2. 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)