I followed the style of auth to only have one definition with the fraction, but have a bunch of lemmas for the special case q = 1. I am not sure if these lemmas carry their weight, but well, now that we already have them I figured we could keep them.
Fixes #356 (closed)