α β : Type u
a : Cardinal
h : a ≠ 0
⊢ 1 ≤ 0 ^< a
α β : Type u
a : Cardinal
h : a ≠ 0
⊢ 0 ^< a = 1
apply (powerlt_le.2 fun c _ => zero_power_le _).antisymm
α β : Type u
a : Cardinal
h : a ≠ 0
⊢ ?m.690119 ^ 0 ≤ 0 ^< a

α β : Type u
a : Cardinal
h : a ≠ 0
⊢ Cardinal
α β : Type u
a : Cardinal
h : a ≠ 0
⊢ 1 ≤ 0 ^< a
rw [← power_zero]
no goals
α β : Type u
a : Cardinal
h : a ≠ 0
⊢ ?m.690119 ^ 0 ≤ 0 ^< a

α β : Type u
a : Cardinal
h : a ≠ 0
⊢ Cardinal
exact le_powerlt 0 (pos_iff_ne_zero.2 h)