proposition: Lemma L_omega_cube_3_eq: let N := exp2 95 in let P := (N * 97 - 1)%nat in L_omega_cube 3 = (exp2 P * (P + 2) - 1)%nat.
proof: Proof. rewrite L_omega_cube_eqn, omega_square_thrice_eqn; [reflexivity | auto with arith]. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)