Clean up Insert Complexity Proof

Remove uses of CpdtTactics and clean up a buncha proofs/reorganize lemmas.