proposition: Lemma H'_omega_i (i:nat) : forall k, H'_ (E0_omega * i)%e0 k = (exp2 i * k + Nat.pred (exp2 i))%nat.
proof: Proof. induction i. - ochange (E0_omega * 0)%e0 E0zero; simpl. intro k; rewrite H'_eq1; abstract lia. - intro k; rewrite H'_eq3. + ochange (Canon (E0_omega * S i)%e0 (S k)) (E0_omega * i + (S k))%e0. rewrite H'_Plus_Fin, IHi. simpl (exp2 (S i)); abstract lia. simpl Canon; destruct i;reflexivity. + reflexivity. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)