Library hydras.solutions_exercises.ge_omega_iff

From hydras Require Import T1 E0.
From Coq Require Import Lia.

Open Scope E0_scope.

Lemma ge_omega_iff (alpha : E0):
  E0_omega o≤ alpha ↔ (∀ i:nat, i + alpha = alpha).