Reintroducing previously deleted lemmas

  These lemmas are present in rls/rls1 but somehow disappeared
  from src/. They are needed for RStirling to compile again.
  There might be more lemmas to salvage. I did not have time to
  investigate.
Uncommenting RStirling and fixing it.