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. auto with T2. nf_inv. intros H1 H2;case H1. nf_inv. destruct 1. discriminate e. left;right. constructor;auto. right. constructor. auto. auto. right. constructor;auto. auto with T2. nf_inv. intros H1 H2;case H1. nf_inv. destruct 1. discriminate e. left;right;constructor. auto. auto. right;constructor;auto. intros. case H1. nf_inv. destruct 1. subst t3;right;constructor;auto. nf_inv. nf_inv. left;right;constructor;auto. right;constructor;auto. Qed.
imports: EPSILON0 Arith List Omega Compare_dec Relations Wellfounded Max Tools More_nat AccP not_decreasing EPSILON0 More_nat Gamma0_prelude Gamma0_length term rpo