Gamma Incomplete Remarks

Stream: PrimeNumberTheorem+

[Steven Rossi]

I just submitted a pr PNT#479 for the first gamma incomplete remark.

I'm not very experience in lean yet, so any advice for cleaning it up would be appreciate. The u-sub implementation seems overly verbose and I'm sure there's a better way to do all the conditions that I'm just not aware of, and then cleaning up the simplifications at the end is definitely doable.