proposition: Lemma canonS_iota_4 : round_n i (iota alpha) (iota (canon alpha (S i))).
proof: Proof. rewrite rem1; subst alpha; simpl. right; right ; right; rewrite <- hcons_mult_comm. apply hcons_mult_S2. left; specialize (Hrec lambda). assert (lambda t1< cons lambda (S n) zero)%t1. { apply head_LT_cons; auto with T1. } specialize (Hrec (T1limit_not_zero Hlambda Hlim) H (canon lambda (S i)) (refl_equal _)). destruct Hrec; [| trivial]; assert False by (eapply limit_no_R1; eauto); contradiction. Qed.
imports: Coq(Relation_Operators) hydras(Hydra_Lemmas Epsilon0 Canon Paths )