auto div_negsuc_negsuc

div_negsuc_negsuc: (all au:UInt, bu:UInt. negsuc(au) / negsuc(bu) = pos((1 + au) / (1 + bu)))

auto div_negsuc_pos

div_negsuc_pos: (all au:UInt, bu:UInt. negsuc(au) / pos(bu) = - pos((1 + au) / bu))

auto div_negsuc_uint

div_negsuc_uint: (all au:UInt, bu:UInt. negsuc(au) / bu = - pos((1 + au) / bu))

auto div_pos_negsuc

div_pos_negsuc: (all au:UInt, bu:UInt. pos(au) / negsuc(bu) = - pos(au / (1 + bu)))

auto div_pos_pos

div_pos_pos: (all au:UInt, bu:UInt. pos(au) / pos(bu) = pos(au / bu))

auto div_pos_uint

div_pos_uint: (all au:UInt, bu:UInt. pos(au) / bu = pos(au / bu))