proposition: Lemma canonS_iota_6 : round_n i (iota alpha) (iota (canon alpha (S i))).
proof: Proof. rewrite rem6; destruct rem62; subst alpha. - simpl iota; left; apply R1_hcons; apply R1_hcons_mult; repeat rewrite iota_iotas. + assumption. + apply nf_canon;auto. + auto. - right; simpl; destruct n. + simpl; replace (hcons (iota beta) (iotas gamma)) with (hy_app (hcons (iota beta) hnil) (iotas gamma)). replace (hcons (iota beta) (iotas (canon gamma (S i)))) with (hy_app (hcons (iota beta) hnil) (iotas (canon gamma (S i)))). apply R2_app; repeat rewrite iota_iotas; auto. eapply nf_canon;auto. simpl; auto. simpl; auto. + replace (hcons (iota beta) (hcons_mult (iota beta) (S n0) (iotas gamma))) with (hy_app (hcons (iota beta) (hcons_mult (iota beta) (S n0) hnil)) (iotas gamma)). replace (hcons (iota beta) (hcons_mult (iota beta) (S n0) (iotas (canon gamma (S i))))) with (hy_app (hcons (iota beta) (hcons_mult (iota beta) (S n0) hnil)) (iotas (canon gamma (S i)))). * apply R2_app;repeat rewrite iota_iotas; auto. eapply nf_canon;auto. * simpl; auto. simpl; auto. repeat f_equal. rewrite <- hcons_mult_app; now simpl hy_app. * rewrite <- hcons_mult_comm; simpl; f_equal. rewrite hcons_mult_comm; simpl; f_equal. now rewrite <- hcons_mult_app. Qed.
imports: Coq(Relation_Operators) hydras(Hydra_Lemmas Epsilon0 Canon Paths )