proposition: Lemma nested_Ack_bound k m n : Ack k (Ack m n) <= Ack (2 + max k m) n.
proof: Proof. pose (x:= Nat.max k m). - fold x. assert (H: m <= x) by lia. assert (H0: k <= x) by lia. simpl (2 + x); transitivity (Ack x (Ack m n)). + apply Ack_mono_l; auto. + transitivity (Ack x (Ack x n)). * apply Ack_mono_r. apply Ack_mono_l; lia. * apply R3. Qed.
imports: Coq(Lia) Coq(Program.Wf Arith) hydras(ssrnat_extracts) Equations(Equations)