Completing Cubical.HITs.CauchyReals

Volume III produced a verdict matrix of 3 valid, 0 invalid, 29 incomplete theorems. A substantial share of the incompletes are blocked on the unmerged Cubical.HITs.CauchyReals module. We complete the missing proofs and prepare the PR for the cubical-agda library.