[Question]: `direct_sum_decomp` interface

[kylechui]

Hey there, I was wondering if there was a particular reason that direct_sum_decomp takes in four arguments? It seems like o, p aren't actually used anywhere. I bring this up because oftentimes when I wish to rewrite direct_sum_decomp., Coq is unable to infer the values of the last two arguments (since they can be anything?), forcing me to write the less-ergonomic rewrite (@direct_sum_decomp _ _ 0 0). From what I can tell, the last two values don't actually matter, so I've set them both to 0.