a div a = 1 by INT_1:49;
hence ( a div a is weightless & a div a is positive ) ; :: thesis: verum