Wrote most of background section, and some of Problem Analysis. Added coqdoc latex files so we can include Coq proofs in Latex. Added diagram for B+ trees.