proposition: Lemma LT_to_standard_battle : forall alpha beta, beta t1< alpha -> exists n i, rounds standard n (iota alpha) i (iota beta).
proof: Proof. intros; assert (nf beta) by eauto with T1. assert (nf alpha) by eauto with T1. assert (Halpha : alpha <> zero) . { intro; subst. apply (not_LT_zero H). } destruct (T1_eq_dec beta zero) as [Hbeta | Hbeta]. { subst beta. destruct (o2iota alpha H1 1). auto. subst; now destruct Halpha. destruct H2. exists 0,x. assumption. } { destruct (Lemma2_6_1 H1 H) as [n Hn]. destruct n. { destruct (constant_to_standard_path H1 Hn). now apply not_zero_lt. exists 0, x. apply o2iota_1. assumption. auto. auto. auto. } { destruct (constant_to_standard_path H1 Hn). now apply not_zero_lt. apply o2iota_1 in s; auto. exists ((S n)), x; auto. } } Qed.
imports: hydras(Epsilon0_Needed_Generic)