assume not a / b is light ; :: thesis: contradiction
then reconsider c = a / b as non light Real ;
( b = 0 implies c = 0 ) ;
then reconsider b = b as non zero Nat ;
c * b = a ;
hence contradiction ; :: thesis: verum