proposition: Lemma H'_omega : forall k, H'_ E0_omega k = S (2 * k)%nat.
proof: Proof. Proof with auto with E0. intro k; rewrite H'_eq3 ... - replace (Canon E0_omega (S k)) with (E0fin (S k)). + rewrite H'_Fin; abstract lia. + now autorewrite with E0_rw. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)