HomeIsabelle/Phabricator

added lemma mono_multp