proposition: Remark Ack_m_mono_weak : forall n p, n <= p -> Ack m n <= Ack m p.
proof: Proof. intros x y H; rewrite -> (Nat.lt_eq_cases x y) in H; destruct H as [H0 | H0]. - apply PeanoNat.Nat.lt_le_incl; auto. destruct Hm as [Hmono _]; now apply Hmono. - subst; now left. Qed.
imports: Coq(Lia) Coq(Program.Wf Arith) hydras(ssrnat_extracts) Equations(Equations)