proposition: Lemma standard_gnaw_to_zero : forall alpha , nf alpha -> forall i, {p:nat | standard_gnaw i alpha p = zero}.
proof: Proof. intro alpha; transfinite_induction alpha. clear alpha; intros alpha Halpha H i. destruct (T1_eq_dec alpha zero) as [e | ne]. - subst alpha; induction i; cbn; now exists 0. - specialize (Halpha (canon alpha i)). assert (canon alpha i t1< alpha)%t1. { destruct i. - apply canon0_LT; auto with T1. - apply canonS_LT; auto. } assert (H1 := nf_canon i H). specialize (Halpha H0 H1 (S i)). destruct Halpha as [x e]; exists (S x); simpl; auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)