Added formatting
Cleaned up lemmaone proof with tactic notation