proposition: Lemma canonS_iota_5 : round_n i (iota alpha) (iota (canon alpha (S i))).
proof: Proof. rewrite rem3; subst alpha. simpl (iota (cons (T1.succ gamma) (S n) zero)); simpl hy_app. assert (R1 (iota (T1.succ gamma)) (iota gamma)). { apply iota_succ_R1; auto. } assert (S1 i (hcons (iota (T1.succ gamma)) hnil) (hcons_mult (iota gamma) (S i) hnil)). { left; auto. } generalize (S1_app i (hcons_mult (iota (T1.succ gamma)) n hnil) _ _ H0); intro H2; right. left; apply S1_next. simpl in H2; simpl. rewrite <- hcons_mult_app in H2. replace (hcons_mult (iota (T1.succ gamma)) n (hy_app hnil (hcons (iota (T1.succ gamma)) hnil))) with (hy_app (hcons_mult (iota (T1.succ gamma)) n hnil) (hcons (iota (T1.succ gamma)) hnil)) in H2. - replace (hcons (iota (T1.succ gamma)) (hcons_mult (iota (T1.succ gamma)) n hnil)) with (hy_app (hcons_mult (iota (T1.succ gamma)) n hnil) (hcons (iota (T1.succ gamma)) hnil)). + apply S1_app; auto. + generalize (iota (T1.succ gamma)) as h;intro. rewrite <- hcons_mult_app. simpl hy_app. now rewrite <- hcons_mult_comm. - generalize (iota (T1.succ gamma)) as h;intro. simpl hy_app; rewrite <- hcons_mult_app. simpl hy_app; auto. Qed.
imports: Coq(Relation_Operators) hydras(Hydra_Lemmas Epsilon0 Canon Paths )