HomeIsabelle/Phabricator

added lemmas totalp_on_multpDM, totalp_multpDM, totalp_on_multpHO, and…