proposition: Lemma Ack_mono_r m: forall n p, n <= p -> Ack m n <= Ack m p.
proof: Proof. intros; apply Ack_m_mono_weak; trivial. apply Ack_properties. Qed.
imports: Coq(Lia) Coq(Program.Wf Arith) hydras(ssrnat_extracts) Equations(Equations)