proposition: Lemma ack_4 : forall b, tower_of_power b <= ack 4 42 (S b).
proof: Proof. intros. rewrite ack_4_aux. rewrite unfold_ack; [|lia]. apply iter_ge_fun. - intro n. apply ack_3. - intros n m le. induction le; auto. replace (42 ^ (S m)) with (42 * (42 ^ m)) by reflexivity. nia. Qed.
imports: Arith Lia