Proof of non_munit_diff_imp_mpdivides