for R being commutative Ring
for r1 being Element of R st r1 in Unit_Set R holds
r1 is right_mult-cancelable