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