n m : ℕ
⊢ Pairwise (fun x x_1 => x < x_1) (range' n (m - n))
n m : ℕ
⊢ Pairwise (fun x x_1 => x < x_1) (Ico n m)
dsimp [Ico]
no goals
n m : ℕ
⊢ Pairwise (fun x x_1 => x < x_1) (range' n (m - n))
simp only [pairwise_lt_range']