proposition: Lemma m_ge_0 alpha: nf alpha -> alpha t1<= m (iota alpha).
proof: Proof. transfinite_induction_lt alpha; clear alpha; intros alpha Hrec H. destruct (T1_eq_dec alpha T1.zero). + subst; repeat split; auto with T1. now apply nf_m . + destruct (T1.zero_limit_succ_dec H). * destruct s. { subst ; now destruct n. } { eapply strict_lub_lub with (s := fun i => canon alpha (S i)). apply canonS_limit_lub; auto. intro i0; assert (round_n i0 (iota alpha) (iota (canon alpha (S i0)))). { apply canonS_iota_i; auto. } apply LE_trans with (m (iota (canon alpha (S i0)))); auto. { apply Hrec; auto. - apply nf_canon; auto. - destruct (canonS_limit_lub H); auto. destruct (H1 i0); tauto. - eapply nf_canon;auto. } apply LE_r; eapply m_decrease; eapply H0. } * destruct s as [x [H0 e]]; subst. assert (x t1< m (iota (T1.succ x))). { apply LE_LT_trans with (m (iota x)). apply Hrec; auto. apply lt_succ; auto. eapply m_decrease. clear Hrec; destruct x. - left; apply iota_succ_R1; eauto. - left; apply iota_succ_R1; eauto. } now apply LT_succ_LE. Unshelve. exact 0. Qed.
imports: hydras(Hydra_Lemmas Epsilon0 Canon Paths O2H) Coq(Relation_Operators)