no goals
ds₁ ds₂ ds₃ is : List ℕ
h : Forall₂ (fun x x_1 => x < x_1) is (ds₁ ++ ds₂ ++ ds₃)
⊢ ↑(drop (drop (assocRight { val := is, property := h }))) = ↑(drop { val := is, property := h })
simp [add_comm, assocRight, drop, cast_type, List.drop_drop]