proposition: Lemma Ack_4_n n : Ack 4 n = hyper_exp2 n.+3 - 3.
proof: Proof. induction n. - reflexivity. - assert (3 <= hyper_exp2 n.+3). { clear IHn; induction n. - cbn; auto with arith. - rewrite hyper_exp2_S; transitivity (hyper_exp2 n.+3); auto. generalize (hyper_exp2 n.+3); intro n0; induction n0. + auto with arith. + assert (0 < exp2 n0). { clear IHn0; induction n0. - cbn;auto. - cbn; lia. } cbn; lia. } rewrite Ack_S_S, IHn. rewrite Ack_3_n; rewrite (hyper_exp2_S n.+3). replace (hyper_exp2 n.+3 - 3).+3 with (hyper_exp2 n.+3); auto. lia. Qed.
imports: Coq(Lia) Coq(Program.Wf Arith) hydras(ssrnat_extracts) Equations(Equations)