proposition: Lemma majorSucc : majorizedPR succFunc Ack.
proof: Proof. exists 1; intro v; rewrite (decomp1 v). simpl evalList; simpl max_v; rewrite Nat.max_0_r. rewrite Ack_1_n; auto with arith. Qed.
imports: hydras(primRec Ack MoreVectors) Coq(Arith ArithRing List Lia Compare_dec)