proposition: Lemma majorPR2_strict (f: naryFunc 2)(Hf : isPR 2 f): exists n:nat, forall x y, 2 <= x -> 2 <= y -> f x y < Ack n (max x y).
proof: Proof. destruct (majorPR2 _ Hf) as [m Hm]. exists (S (max 2 m)); intros x y; destruct x, y; try lia. intros _ _; apply Nat.le_lt_trans with (Ack m (S (Nat.max x y))). - rewrite Nat.succ_max_distr; auto. - rewrite Nat.succ_max_distr; apply Ack_strict_mono_l; lia. Qed.
imports: hydras(primRec Ack MoreVectors) Coq(Arith ArithRing List Lia Compare_dec)