# `Finset.range` and addition of natural numbers #

source
theorem Finset.disjoint_range_addLeftEmbedding (a : ℕ) (s : Finset ℕ) :
Disjoint (range a) (map (addLeftEmbedding a) s)
source
theorem Finset.disjoint_range_addRightEmbedding (a : ℕ) (s : Finset ℕ) :
Disjoint (range a) (map (addRightEmbedding a) s)
source
theorem Finset.range_add (a b : ℕ) :
range (a + b) = range a ∪ map (addLeftEmbedding a) (range b)