proposition: Lemma F_alpha_notPR_inv: forall alpha, (isPR 1 (F_ alpha) -> False) -> E0_omega o<= alpha.
proof: Proof. intros alpha H; destruct (E0_lt_ge alpha E0_omega); auto. destruct (lt_omega_inv H0) as [i Hi]; subst alpha. destruct H; apply F_n_PR. Qed.
imports: hydras(Iterates F_alpha E0 Ack AckNotPR) Coq(ArithRing Lia Arith)