proposition: Lemma Ack_strict_mono_l : forall n m p, n < m -> Ack n p.+1 < Ack m p.+1.
proof: Proof. induction 1. - apply R5. - transitivity (Ack m p.+1); auto. apply R5. Qed.
imports: Coq(Lia) Coq(Program.Wf Arith) hydras(ssrnat_extracts) Equations(Equations)