n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ l ≤ k
n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ ¬decide (k < l) = true
simp only [decide_eq_true_eq, not_lt]
n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ n ≤ k
n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ l ≤ k
apply le_trans hln
no goals
n m l : ℕ
hln : l ≤ n
k : ℕ
hk : k ∈ Ico n m
⊢ n ≤ k
exact (mem.1 hk).1