rewrite the current goal using (double_minus_one_map_apply (eps_ 1) eps_1_in_unit_interval_right_half) (from left to right).

rewrite the current goal using eps_1_half_eq2 (from left to right).

rewrite the current goal using (add_SNo_minus_SNo_rinv 1 SNo_1) (from left to right).