proposition: Remark R4 : F_ 3 2 = F_ 2 (F_ 2 (F_ 2 2)).
proof: Proof. ochange (E0fin 3) (E0_succ 2). rewrite F_succ_eqn. do 3 rewrite iterate_S_eqn. reflexivity. Qed.
imports: hydras(Iterates F_alpha E0) Coq(ArithRing Lia Max) Coq(Mult)