case pos
a : Ordinal
h : a = 0
⊢ a ^ 0 = 1

case neg
a : Ordinal
h : ¬a = 0
⊢ a ^ 0 = 1
a : Ordinal
⊢ a ^ 0 = 1
by_cases h : a = 0
no goals
case pos
a : Ordinal
h : a = 0
⊢ a ^ 0 = 1
simp only [opow_def, if_pos h, sub_zero]
no goals
case neg
a : Ordinal
h : ¬a = 0
⊢ a ^ 0 = 1
simp only [opow_def, if_neg h, limitRecOn_zero]