proposition: Lemma majorPR1 (f: naryFunc 1)(Hf : isPR 1 f) : exists (n:nat), forall x, f x <= Ack n x.
proof: Proof. destruct Hf as [x Hx]. generalize (majorAnyPR 1 x). intros. destruct H as [N HN]. exists N. intros x0; specialize (HN [x0]); cbn in HN. replace (evalPrimRec 1 x x0) with (f x0 ) in HN. now rewrite Nat.max_0_r in HN. symmetry; apply Hx. Qed.
imports: hydras(primRec Ack MoreVectors) Coq(Arith ArithRing List Lia Compare_dec)