Strong Subadditivity #9
Description
Could follow e.g. this proof. Lieb's inequality has been stubbed out alright in the repo. I'm okay leaving these necessary mathlibbable theorems as sorries for now, since they might require a good bit of operator theory that's not easy at the moment.