a b c : Ordinal
ab : a < b
⊢ a ^ c * a < b ^ c * b
a b c : Ordinal
ab : a < b
⊢ a ^ succ c < b ^ succ c
rw [opow_succ, opow_succ]
no goals
a b c : Ordinal
ab : a < b
⊢ a ^ c * a < b ^ c * b
exact
  (mul_le_mul_right' (opow_le_opow_left c ab.le) a).trans_lt
    (mul_lt_mul_of_pos_left ab (opow_pos c ((Ordinal.zero_le a).trans_lt ab)))