did "Proof by Simplification" and "Proof by Case Analysis." stuck on proving commutativity of beq_nat. starting exercises