Recursion on the natural numbers and Set.range

theorem Nat.zero_union_range_succ : {0} ∪ Set.range Nat.succ = Set.univ

@[simp]

theorem Nat.range_succ : Set.range Nat.succ = {i : ℕ | 0 < i}

theorem Nat.range_of_succ {α : Type u_1} (f : ℕ → α) : {f 0} ∪ Set.range (f ∘ Nat.succ) = Set.range f

theorem Nat.range_rec {α : Type u_2} (x : α) (f : ℕ → α → α) : (Set.range fun (n : ℕ) => Nat.rec x f n) = {x} ∪ Set.range fun (n : ℕ) => Nat.rec (f 0 x) (f ∘ Nat.succ) n

theorem Nat.range_casesOn {α : Type u_2} (x : α) (f : ℕ → α) : (Set.range fun (n : ℕ) => Nat.casesOn n x f) = {x} ∪ Set.range f