slice is a conv tactic; if the current focus is a composition of several morphisms,
slice a b reassociates as needed, and zooms in on the a-th through b-th morphisms.
Thus if the current focus is (a ≫ b) ≫ ((c ≫ d) ≫ e), then slice 2 3 zooms to b ≫ c.
slice_lhs a b { tac } zooms to the left hand side, uses associativity for categorical
composition as needed, zooms in on the a-th through b-th morphisms, and invokes tac.
slice_rhs a b { tac } zooms to the right hand side, uses associativity for categorical
composition as needed, zooms in on the a-th through b-th morphisms, and invokes tac.