case h.e'_4
b u v w : Ordinal
hvb : v < b
hw : w < b ^ u
⊢ b ^ succ u = b ^ u * b
b u v w : Ordinal
hvb : v < b
hw : w < b ^ u
⊢ b ^ u * v + w < b ^ succ u
convert (opow_mul_add_lt_opow_mul_succ v hw).trans_le (mul_le_mul_left' (succ_le_of_lt hvb) _)
  using 1
no goals
case h.e'_4
b u v w : Ordinal
hvb : v < b
hw : w < b ^ u
⊢ b ^ succ u = b ^ u * b
exact opow_succ b u