proposition: Lemma H'_Phi0_succ_0 : forall k, H'_ (E0_phi0 (E0_succ E0zero)) k = H'_succ_fun (H'_ (E0_phi0 E0zero)) k.
proof: Proof. Proof with auto with E0. intros k. replace (E0_phi0 E0zero) with (E0fin 1). replace (E0_phi0 (E0_succ E0zero)) with E0_omega. rewrite H'_omega. unfold H'_succ_fun. transitivity (iterate S (S k) k). replace (S (2 * k))%nat with (S k + k)%nat. generalize (S k). induction n. now cbn. cbn. now rewrite IHn. lia. apply iterate_ext. intro x. now rewrite H'_Fin. apply E0_eq_intro. reflexivity. apply E0_eq_intro. reflexivity. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)