proposition: Lemma Ack_3_n n: Ack 3 n = exp2 n.+3 - 3.
proof: Proof. induction n. - reflexivity. - rewrite Ack_S_S, Ack_2_n, IHn. change (exp2 n.+4) with (2 * exp2 n.+3). assert (3 <= exp2 n.+3). { clear IHn;induction n; cbn. - auto with arith. - cbn in IHn; lia. } lia. Qed.
imports: Coq(Lia) Coq(Program.Wf Arith) hydras(ssrnat_extracts) Equations(Equations)