proposition: Lemma ack_nest_bound i1 i2 j: ack(i1, ack(i2,j)) < ack(2 + i1 + i2, j).
proof: Proof. assert (ack (i1, ack (i2, j)) < ack(i1 + i2, ack(S (i1 + i2), j))). { eapply Nat.le_lt_trans. apply ack_le_mono1. 2: apply ack_lt_mono2. - apply le_add_r. - apply ack_lt_mono1. auto with arith. } eapply Nat.lt_le_trans. apply H. rewrite <- ack_equation_3. apply ack2_le_ack1. Qed.
imports: Arith Lia Equations(Equations)