HomeIsabelle/Phabricator

added lemma multpHO_plus_plus[simp]