implicit arguments in quotient.v, close #447

I made it local because it looked to me like a temporary shorthand notation that shoudn't be cluttering up the global namespace.  I do agree it's an important notion that should have a global name, but I think it would be more appropriate to define it somewhere else (Overture, maybe, or Trunc), and to give it a more descriptive name.