proposition: Lemma standard_path_to_zero: forall alpha i, nf alpha -> alpha <> zero -> {j: nat | standard_path (S i) alpha j zero}.
proof: Proof. intro alpha; transfinite_induction alpha; clear alpha; intros alpha Halpha i H. destruct (T1_eq_dec alpha zero). - subst; exists (S i); replace zero with (canon zero (S i)) at 2. + left; trivial. * discriminate. + reflexivity. - intros _; destruct (T1_eq_dec (canon alpha (S i)) zero). + exists (S i); left; auto. + specialize (Halpha (canon alpha (S i)) (canonS_LT i H n) (S i)). destruct Halpha; auto. * apply nf_canon; auto. * exists x; right; auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)