z < ∞ → x1 + z + y1 = x2 + z + y2 → x1 + y1 = x2 + y2.
#z #x1 #x2 #y1 #y2 #Hz
<yplus_plus_comm_23 <yplus_plus_comm_23 in ⊢ (???%→?); #H
z < ∞ → x1 + z + y1 = x2 + z + y2 → x1 + y1 = x2 + y2.
#z #x1 #x2 #y1 #y2 #Hz
<yplus_plus_comm_23 <yplus_plus_comm_23 in ⊢ (???%→?); #H