proposition: Lemma o2iota_0 : forall j beta i alpha, standard_path_to j beta i alpha -> (0 < i)%nat -> nf alpha -> nf beta -> beta <> T1.zero -> rounds standard (Nat.pred i) (iota alpha) j (iota beta) .
proof: Proof. induction 1. - intros; subst j; destruct i. + now destruct H2. + simpl; left; trivial. * subst beta; apply canonS_iota_i; trivial. - intros H0 H1 H2 H3; destruct i. + inversion H0. + eapply rounds_trans with (S i) (iota (canon alpha (S i))); trivial. 2:(left; simpl); trivial. replace (S i) with (Nat.pred (S (S i))). * eapply IHstandard_path_to; trivial. auto with arith. eapply nf_canon;eauto. * simpl; auto. * apply canonS_iota_i; trivial. intro; subst alpha. apply H3; eapply standard_path_zero; eauto. Qed.
imports: hydras(Epsilon0_Needed_Generic)