b : Ordinal
⊢ 0 ^ succ b = 0 ^ b * 0
a b : Ordinal
h : a = 0
⊢ a ^ succ b = a ^ b * a
subst a
no goals
b : Ordinal
⊢ 0 ^ succ b = 0 ^ b * 0
simp only [zero_opow (succ_ne_zero _), mul_zero]
no goals
a b : Ordinal
h : ¬a = 0
⊢ a ^ succ b = a ^ b * a
simp only [opow_def, limitRecOn_succ, if_neg h]