explicitly name hypotheses

Please do not rely on naming schemes by Coq, that is, do not assume
that Coq will call the introduced hypotheses `H0`. Give it an explicit
name.
Simplify the Archimedan axioms.

It turns out we do not need to work with proofs of positivity, which
makes the proofs of Archimedean property much nicer.