m n k l : ℕ
⊢ m = n + 1 → n ≤ m
m n k l : ℕ
⊢ n ≤ m ∧ m ≤ n + 1 ↔ m = n ∨ m = n + 1
rw [le_add_one_iff, and_or_left, ← le_antisymm_iff, eq_comm, and_iff_right_of_imp]
n k l : ℕ
⊢ n ≤ n + 1
m n k l : ℕ
⊢ m = n + 1 → n ≤ m
rintro rfl
no goals
n k l : ℕ
⊢ n ≤ n + 1
exact n.le_succ