HomeIsabelle/Phabricator

added lemma irreflp_on_multpHO[simp]