The increasing enumeration of the divisors of a natural number

Basic facts about Nat.nth (· ∈ n.divisors), the increasing enumeration of the divisors of n.

theorem Nat.nth_divisors_zero {n : ℕ} (hn : n ≠ 0) : nth (fun (x : ℕ) => x ∈ n.divisors) 0 = 1

The smallest divisor of a positive number is 1, i.e. the 0th entry of the increasing enumeration of its divisors.

theorem Nat.two_le_nth_divisors {n : ℕ} (hn : n ≠ 0) {i : ℕ} (hi : i ≠ 0) (h : nth (fun (x : ℕ) => x ∈ n.divisors) i ≠ 0) : 2 ≤ nth (fun (x : ℕ) => x ∈ n.divisors) i

Every divisor enumerated after index 0 is at least 2.