proposition: Lemma majorProjection (n m:nat)(H: m < n): majorizedPR (projFunc n m H) Ack.
proof: Proof. red; cbn; red; exists 0. rewrite Ack_0; intro v; transitivity (max_v v). + apply proj_le_max. + auto with arith. Qed.
imports: hydras(primRec Ack MoreVectors) Coq(Arith ArithRing List Lia Compare_dec)