proposition: Lemma Ack_mono_l m n : m <= n -> forall p, Ack m p <= Ack n p.
proof: Proof. induction 1; auto. intro p; transitivity (Ack m0 p); auto. destruct (Ack_properties m0) as [_ [_ H0]]; auto. Qed.
imports: Coq(Lia) Coq(Program.Wf Arith) hydras(ssrnat_extracts) Equations(Equations)