In this file we apply metric.complete_of_cauchy_seq_tendsto to prove that a normed_ring
is complete in terms of cauchy filter if and only if it is complete in terms
of cau_seq Cauchy sequences.
In a normed field, cau_seq 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.