fact: Definition majorizedS {n m} (fs : Vector.t (naryFunc n) m) (A : naryFunc 2):= exists N, forall (v: t nat n), max_v (Vector.map (fun f => v_apply f v) fs) <= A N (max_v v).
imports: hydras(primRec Ack MoreVectors) Coq(Arith ArithRing List Lia Compare_dec)