step a s n : Nat
h : a ≤ s
⊢ map (fun x => x - a) (range' (a + (s - a)) n step) = range' (s - a) n step
step a s n : Nat
h : a ≤ s
⊢ map (fun x => x - a) (range' s n step) = range' (s - a) n step
conv => lhs; rw [← Nat.add_sub_cancel' h]
step a s n : Nat
h : a ≤ s
⊢ ((fun x => x - a) ∘ fun x => a + x) = id
step a s n : Nat
h : a ≤ s
⊢ map (fun x => x - a) (range' (a + (s - a)) n step) = range' (s - a) n step
rw [← map_add_range', map_map, (?_ : _∘_ = _), map_id]
case h
step a s n : Nat
h : a ≤ s
x : Nat
⊢ ((fun x => x - a) ∘ fun x => a + x) x = id x
step a s n : Nat
h : a ≤ s
⊢ ((fun x => x - a) ∘ fun x => a + x) = id
funext x
no goals
case h
step a s n : Nat
h : a ≤ s
x : Nat
⊢ ((fun x => x - a) ∘ fun x => a + x) x = id x
apply Nat.add_sub_cancel_left