proposition: Remark R5 m n : Ack m n.+1 < Ack m.+1 n.+1.
proof: Proof. rewrite Ack_S_S; apply Ack_strict_mono. apply Nat.le_lt_trans with (m.+1 + n). - lia. - apply Ack_Sn_plus. Qed.
imports: Coq(Lia) Coq(Program.Wf Arith) hydras(ssrnat_extracts) Equations(Equations)