proposition: Fact F2 : H'_ (E0_phi0 3 + 3) 0 = f (f N).
proof: Proof. rewrite H'_Plus_Fin, Nat.add_0_r, F1; reflexivity. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)