a b : ℕ
⊢ Disjoint (range a) (map (fun x => a + x) (range b))
a b : ℕ
⊢ range (a + b) = range a ∪ map (fun x => a + x) (range b)
rw [range_add, add_eq_union_iff_disjoint]
no goals
a b : ℕ
⊢ Disjoint (range a) (map (fun x => a + x) (range b))
apply range_disjoint_map_add