proposition: Lemma standard_gnaw_2_zero : forall alpha i, nf alpha -> {t: nat | standard_gnaw i alpha t = zero }.
proof: Proof. intro alpha; transfinite_induction alpha. clear alpha; intros alpha Halpha i H. destruct (T1_eq_dec alpha zero). - subst; exists 0; trivial. - specialize (Halpha (canon alpha i)). assert (LT (canon alpha i) alpha). { destruct i. apply canon0_LT; eauto with T1. apply canonS_LT; eauto with T1. } destruct (Halpha H0 (S i)) as [x Hx]. * apply nf_canon;auto. * now exists (S x). Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)