Reorganized formalization in different theories. Some proofs are pending, and the formalization needs to be recast into locales.