proposition: Lemma Winner : forall alpha, nf alpha -> Hercules_ok alpha.
proof: Proof. intros o Ho; apply EPSILON0.transfinite_induction. 2:auto. intros. unfold Hercules_ok. destruct h. constructor. unfold Hercules_ok in H0. intro. right. intros. generalize (H0 (h2o h') ). intros; eapply H0. 3:reflexivity. apply h2o_nf. case H1. eapply Rh_decrease. eauto. Qed.
imports: Arith Omega List EPSILON0 MSE0