α β : Type u
m n : ℕ
⊢ ↑m ≤ ↑n ∧ ¬↑n ≤ ↑m ↔ ¬n ≤ m
α β : Type u
m n : ℕ
⊢ ↑m < ↑n ↔ m < n
rw [lt_iff_le_not_le, ← not_le]
α β : Type u
m n : ℕ
⊢ m < n → m ≤ n
α β : Type u
m n : ℕ
⊢ ↑m ≤ ↑n ∧ ¬↑n ≤ ↑m ↔ ¬n ≤ m
simp only [natCast_le, not_le, and_iff_right_iff_imp]
no goals
α β : Type u
m n : ℕ
⊢ m < n → m ≤ n
exact fun h ↦ le_of_lt h