proposition: Lemma Ack_Sn_plus : forall n p, n.+1 + p < Ack n.+1 p.
proof: Proof. induction n. - intro; rewrite Ack_1_n; lia. - induction p. + rewrite Ack_S_0. specialize (IHn 1); lia. + rewrite Ack_S_S. assert (Ack n.+2 p < Ack n.+1 (Ack n.+2 p)). { destruct (Ack_properties n.+1) as [H [H0 H1]]; apply H0. } eapply Nat.le_lt_trans with (2:= H). replace (n.+2 + p.+1) with (n.+3 + p) by lia. apply IHp. Qed.
imports: Coq(Lia) Coq(Program.Wf Arith) hydras(ssrnat_extracts) Equations(Equations)