a b : Ordinal
ha : 0 < a
⊢ a * b ≤ b ↔ a * b = b
a b : Ordinal
ha : 0 < a
⊢ a * b ≤ b ↔ a ^ ω ∣ b
rw [← mul_eq_right_iff_opow_omega_dvd]
no goals
a b : Ordinal
ha : 0 < a
⊢ a * b ≤ b ↔ a * b = b
exact (mul_isNormal ha).le_iff_eq