Finset.range and addition of natural numbers

theorem Finset.disjoint_range_addLeftEmbedding (a : ℕ) (s : Finset ℕ) : Disjoint (range a) (map (addLeftEmbedding a) s)

theorem Finset.disjoint_range_addRightEmbedding (a : ℕ) (s : Finset ℕ) : Disjoint (range a) (map (addRightEmbedding a) s)

theorem Finset.range_add (a b : ℕ) : range (a + b) = range a ∪ map (addLeftEmbedding a) (range b)