Commit before trying to get metric and setoids working, again.
Getting rid of Lipschitz and Metric stuff.
Reverting to doing things by hand.

It seems quite complicated to get the Lipschitz maps working. So we are
going to try to do everything with bare hands. It does not seem so bad,
actually.
Merge branch 'master' of github.com:andrejbauer/dedekind-reals

Conflicts:
	Arithmetic.v