n m : ℕ
hnm : n < m
r : min m (n + 1) = n + 1
⊢ filter (fun x => decide (x < n + 1)) (Ico n m) = [n]
n m : ℕ
hnm : n < m
⊢ filter (fun x => decide (x < n + 1)) (Ico n m) = [n]
have r : min m (n + 1) = n + 1 := (@inf_eq_right _ _ m (n + 1)).mpr hnm
no goals
n m : ℕ
hnm : n < m
r : min m (n + 1) = n + 1
⊢ filter (fun x => decide (x < n + 1)) (Ico n m) = [n]
simp [filter_lt n m (n + 1), r]