exact le_trans (Nat.pow_le_pow_right (Nat.zero_lt_succ 0) (Nat.succ_le_succ (Nat.zero_le _))) (Nat.pow_le_pow_left (Nat.succ_le_succ (Nat.zero_le _)) _)
case succ.succ.succ
n✝² n✝¹ n✝ : ℕ
⊢ 1 ≤ Nat.succ n✝ ^ Nat.succ n✝¹
no goals