proved that Cauchy and limit define the same completion
added prop relating Cauchy sequences and completions; expanded the proof that completions are complete