removed unnecessary lemma Max_Im_ge_other_Im1
documented lemma Max_Im_imp_ex_elem
renamed lemma Max_Im_ge_other_Im2 → Max_Im_ge_other_Im and documented
documented lemma Max_Im_ge
now documented most steps of wd_outcome proof