m n✝ k n : ℕ
x✝² : n + 3 ≠ 0
x✝¹ : n + 3 ≠ 1
x✝ : n + 3 ≠ 2
⊢ 2 + 1 ≤ n + 3
m n✝ k n : ℕ
x✝² : n + 3 ≠ 0
x✝¹ : n + 3 ≠ 1
x✝ : n + 3 ≠ 2
⊢ 2 < n + 3
rw [Nat.lt_iff_add_one_le]
no goals
m n✝ k n : ℕ
x✝² : n + 3 ≠ 0
x✝¹ : n + 3 ≠ 1
x✝ : n + 3 ≠ 2
⊢ 2 + 1 ≤ n + 3
convert Nat.le_add_left 3 n