proposition: Lemma ack_3 : forall a b, a ^ b <= ack 3 a b.
proof: Proof. intros; rewrite ack_3_aux. apply iter_ge_fun. - intro n. induction n; try lia. simpl. replace (a * S n) with (a + (a * n)) by ring. lia. - intros n m; nia. Qed.
imports: Arith Lia