chore(data/option): swap sides in `ne_none_iff_exists` (#4285)
* swap lhs and rhs of the equality in `option.ne_none_iff_exists`; the new order matches, e.g., the definition of `set.range` and `can_lift.prf`;
* the same in `with_one.ne_one_iff_exists` and `with_zero.ne_zero_iff_exists`;
* remove `option.ne_none_iff_exists'`;
* restore the original `option.ne_none_iff_exists` as `option.ne_none_iff_exists'`
