Replace confusing absolute value signs

[jim-portegies]

Some things to think about:

1. In the definition of convergence, would it be better to immediately go to absolute value of the difference? The downside is that it doesn't fully correspond to the definition of convergence. The upside is that arguments become a bit simpler.
2. Depending on the answer to 1, some elements need to be added to the "expand" mechanism.
3. Not for this PR, but maybe we should add a normalization step into our automation (that does all the unfolds that we want to do by default)

[pimotte]

LGTM. (One suggestion for a comment).

Do note that this breaks some exercise sheets, but that's also the point. I don't think we want to try updating coq-waterproof mid-course for this, so maybe we should keep the adapted sheets in a branch.

I think going directly to absolute values should depend on the didactics. If you teach with the general definition in the metric space, I think it makes sense to add an alternative characterization that goes straight to absolute values.

With respect to normalization: I think this makes sense, but it's something I would put on low prio: It's a lot of work and I'm not sure it will have a large impact.

[pimotte]

Suggested change

	Notation "| x |" := (Rabs x) (at level 20, format "| x |") : R_scope.
	(* The symbol below is the standard pipe, unicode codepoint: U+007C *)
	Notation "| x |" := (Rabs x) (at level 20, format "| x |") : R_scope.