reconsider b = 1 / a as positive light Real ;
1 div a = [\(1 / a)/] by INT_1:def 9
.= 0 ;
hence 1 div a is zero ; :: thesis: verum