Record is_CMetricField (F : CField) (abs : CSetoid_fun F IR) : Prop :=
{ax_abs_gt_zero : forall x : F, 0 [<=] abs x;
ax_abs_resp_mult : forall x y : F, abs (x[*]y) [=] abs x[*]abs y;
ax_abs_triangle : forall x y : F, abs (x[+]y) [<=] abs x[+]abs y}.
Record CMetricField : Type :=
{cmf_crr :> CField;
cmf_abs : CSetoid_fun cmf_crr IR;
cmf_proof : is_CMetricField cmf_crr cmf_abs}.
End CMetric_Fields.
Notation MAbs := (cmf_abs _).
Section basics.
Lemma MAbs_one : forall F : CMetricField,
{MAbs (1:F) [=] 0} + {MAbs (1:F) [=] 1}.
Lemma MAbs_one_recip_one : forall F : CMetricField,
MAbs (1:F) [=] MAbs ( [--]1:F).
End basics.
Section CMetric_Field_Cauchy.
Variable F : CMetricField.
Let F:CMetricField.
Definition MCauchy_prop (g : N -> F) : CProp := forall e : IR,
0 [<] e -> {N : N | forall m, N <= m -> MAbs (g m[-]g N) [<=] e}.
Record MCauchySeq : Type :=
{MCS_seq :> N -> F;
MCS_proof : MCauchy_prop MCS_seq}.
Definition MseqLimit (seq : N -> F) (lim : F) : CProp := forall e : IR,
0 [<] e -> {N : N | forall m, N <= m -> MAbs (seq m[-]lim) [<=] e}.
Definition is_MCauchyCompl (lim : MCauchySeq -> F) : CProp :=
forall (s : MCauchySeq), MseqLimit s (lim s).
End CMetric_Field_Cauchy.