proposition: Lemma F_omega_not_PR : False.
proof: Proof. destruct (majorPR1 _ F_omega_PR) as [n Hn]; specialize (Hn (S n)). assert (n <> 0). { intro; subst; cbn in Hn; rewrite F_lim_eqn in Hn. - rewrite Canon.Canon_Omega in Hn. rewrite LF1 in Hn; lia. - reflexivity. } specialize (F_vs_Ack (S n)). intros H0; assert (H1: 2 <= S n) by lia. apply H0 in H1; clear H0. assert(Ack n (S n) < Ack (S n) (S n)) by (apply Ack_strict_mono_l; auto). lia. Qed.
imports: hydras(Iterates F_alpha E0 Ack AckNotPR) Coq(ArithRing Lia Arith)