[GOAL]
n : ℕ
⊢ range (succ n) = n ::ₘ range n
[PROOFSTEP]
rw [range, List.range_succ, ← coe_add, add_comm]
[GOAL]
n : ℕ
⊢ ↑[n] + ↑(List.range n) = n ::ₘ range n
[PROOFSTEP]
rfl
[GOAL]
a : ℕ
m : Multiset ℕ
⊢ Disjoint (range a) (map (fun x => a + x) m)
[PROOFSTEP]
intro x hxa hxb
[GOAL]
a : ℕ
m : Multiset ℕ
x : ℕ
hxa : x ∈ range a
hxb : x ∈ map (fun x => a + x) m
⊢ False
[PROOFSTEP]
rw [range, mem_coe, List.mem_range] at hxa 
[GOAL]
a : ℕ
m : Multiset ℕ
x : ℕ
hxa : x < a
hxb : x ∈ map (fun x => a + x) m
⊢ False
[PROOFSTEP]
obtain ⟨c, _, rfl⟩ := mem_map.1 hxb
[GOAL]
case intro.intro
a : ℕ
m : Multiset ℕ
c : ℕ
left✝ : c ∈ m
hxa : a + c < a
hxb : a + c ∈ map (fun x => a + x) m
⊢ False
[PROOFSTEP]
exact (self_le_add_right _ _).not_lt hxa
[GOAL]
a b : ℕ
⊢ range (a + b) = range a ∪ map (fun x => a + x) (range b)
[PROOFSTEP]
rw [range_add, add_eq_union_iff_disjoint]
[GOAL]
a b : ℕ
⊢ Disjoint (range a) (map (fun x => a + x) (range b))
[PROOFSTEP]
apply range_disjoint_map_add
