Blaisorblade

Require Import ssreflect.

Fixpoint ackn (m : nat) (ack : nat -> nat) {struct m} :=
  match m with
  | O => ack 1
  | S q => ack (ackn q ack)
  end.
Fixpoint ack (n m : nat) {struct n} : nat :=
  match n with
  | O => S m