proposition: Lemma geS_ack : forall n a, 2 <= a -> geS (ack n a).
proof: Proof. induction n; intros. - intro; simpl; lia. - intro b. case n as [|n]; [simpl; lia|]. induction b; [simpl; now auto|]. case n as [|n]. + rewrite ack_2. nia. + rewrite unfold_ack; [|lia]. rewrite unfold_iter. transitivity (S (ack (3 + n) a b)). -- apply le_n_S. apply IHb. -- apply IHn. auto. Qed.
imports: Arith Lia