proposition: Lemma KS_thm_2_4_lemma2 (n:nat)(alpha:T1) : nf alpha -> alpha <> zero -> const_pathS n alpha zero.
proof: Proof. transfinite_induction alpha; clear alpha; intros alpha hrec Halpha. destruct (zero_limit_succ_dec Halpha). - destruct s. + intro; contradiction. + intros; specialize (hrec (canon alpha (S n))); constructor 2 with (canon alpha (S n)). * split;trivial. * apply hrec. -- apply canonS_LT;auto. -- eapply nf_canon; eauto. -- now apply T1limit_canonS_not_zero. - destruct s as [beta [Hbeta e]]; subst. destruct (T1_eq_dec beta zero). + subst; left; split; auto. + right with beta. * split; auto. now rewrite canon_succ. * apply hrec; auto with T1. now apply LT_succ. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)