Proof of set_blt_functionality_wrt_set_lt_r