feat(Algebra/Order/Sub/Canonical): add tsub_tsub_eq_add_tsub_of_le (#8804)
tsub_tsub_eq_add_tsub_of_le