proposition: Lemma ack_add_bound i1 i2 j: ack(i1,j) + ack(i2,j) < ack (4 + i1 + i2, j).
proof: Proof. apply (lt_trans _ (ack(2, ack(i1 + i2, j))) _). - rewrite ack_2. pose (H1 := ack_le_mono1 j i1 (i1 + i2)). pose (H2 := ack_le_mono1 j i2 (i1 + i2)). lia. - apply ack_nest_bound. Qed.
imports: Arith Lia Equations(Equations)