Cache intermediate values for Edwards addition

[bMacSwigg]

Creates a new "cached" point type, which holds the computed values of (x-y)/2 and (x+y)/2. Addition is then split into the "prep" function to create a cached point, and the "readdition" function to add a point to a cached point. This proves that the combination m1readd(P, m1prep(Q)) is equivalent to the straightforward add function m1add(P,Q).

This file reuses some of the definitions, proofs, etc. from Basic.v, but for annoying Context reasons some of them had to be copied into this file. There's probably a way to share or reuse them, but it didn't seem worth blocking this change on.

This also doesn't prove Proper_cached_to_twisted, which we might want down the line. My straightforward attempt at copying Proper_to_twisted hit a snag, and nothing in this file actually needed to use it, so I left that out.