In this file we apply Metric.complete_of_cauchySeq_tendsto to prove that a NormedRing
is complete in terms of Cauchy filter if and only if it is complete in terms
of CauSeq Cauchy sequences.
In a normed field, CauSeq coincides with the usual notion of Cauchy sequences.
A complete normed field is complete as a metric space, as Cauchy sequences converge by
assumption and this suffices to characterize completeness.