proposition: Lemma dom_AckNotPR: isPR 1 f -> False.
proof: Proof. intros H; destruct Hf as [n Hn]. destruct (majorPR1 _ H) as [m Hm]. pose (x := Nat.max n m). specialize (Hn x (Nat.le_max_l n m)); cbn in Hn; specialize (Hm x). assert (Ack m x <= Ack x x) by (apply Ack_mono_l; subst; lia). lia. Qed.
imports: hydras(primRec Ack MoreVectors) Coq(Arith ArithRing List Lia Compare_dec)