proposition: Lemma ack2_le_ack1 i j: ack (i, S j) <= ack (S i, j).
proof: Proof. induction j; simp ack. - constructor. - apply ack_le_mono2. eapply le_trans. exact (lt_ack2 i (S j)). exact IHj. Qed.
imports: Arith Lia Equations(Equations)