n m l : ℕ
hml : m ≤ l
k : ℕ
hk : k ∈ Ico n m
⊢ ¬l ≤ k
n m l : ℕ
hml : m ≤ l
k : ℕ
hk : k ∈ Ico n m
⊢ ¬decide (l ≤ k) = true
rw [decide_eq_true_eq]
no goals
n m l : ℕ
hml : m ≤ l
k : ℕ
hk : k ∈ Ico n m
⊢ ¬l ≤ k
exact not_le_of_gt (lt_of_lt_of_le (mem.1 hk).2 hml)