Comment by or_am_i

Lemmas ~ library code, theorems ~ application code.