Homework 2 We get started with formalizing some propositions and workings with our first tactics to give proofs.