Added examples of projections lemma, and started a documentation files detailling each of the tacticals