proposition: Remark R0 (m:nat): forall n, 2 + n <= Ack (2 + m) n.
proof: Proof. induction m. - intros; simpl (2+0). induction n; auto with arith. rewrite Ack_S_S. transitivity (Ack 0 (Ack 2 n)). + rewrite Ack_0; lia. + apply Ack_mono_l; auto. - replace (2 + S m) with (S (2 + m)) by lia. destruct (Ack_properties (2+m)) as [_ [H1 H2]]. intro n; transitivity (Ack (2 + m) n); auto. Qed.
imports: Coq(Lia) Coq(Program.Wf Arith) hydras(ssrnat_extracts) Equations(Equations)