proposition: Lemma ge_omega_iff (alpha : E0): E0_omega o<= alpha <-> (forall i:nat, i + alpha = alpha).
proof: Proof. destruct alpha as [a Ha]; unfold E0le; cbn. destruct a; cbn; split; intros H. - rewrite Le_iff in H; destruct H as (H, (Hle, Hnf)). now apply le_zero_inv in Hle. - specialize (H 1); compute in H; now injection H. - intros i; apply E0_eq_intro. destruct i; auto. destruct a1; auto. rewrite Le_iff in H; cbn in H. destruct H, H0; rewrite le_lt_eq in H0. destruct H0; discriminate. - destruct a1. + specialize (H 1); cbn in H. assert (a2 = zero) by (eapply nf_of_finite; eauto). subst; compute in H; inversion H; lia. + rewrite Le_iff; cbn. apply LE_trans with (T1.phi0 (cons a1_1 n0 a1_2)). * repeat split; auto. apply T1.phi0_mono; apply le_trans with (cons a1_1 0 zero). -- apply T1.phi0_mono; auto with T1. -- apply le_phi0. -- apply nf_phi0; eauto with T1. * repeat split; eauto with T1. apply le_phi0. Qed.
imports: hydras(T1 E0) Coq(Lia)