HomeIsabelle/Phabricator

added lemmas total_on_mult, total_mult, totalp_on_multp, and totalp_multp