HomeIsabelle/Phabricator

added lemmas monotone_on_empty[simp] and monotone_on_subset