proposition: Lemma C_dist_refl : forall a b, C_dist a b = 0%R <-> a = b.
proof: Proof. intros a b ; split ; intro H. assert (M := Cnorm_0 _ H) ; apply Cminus_diag_uniq ; assumption. unfold C_dist ; subst ; unfold Cminus ; rewrite Cadd_opp_r ; apply Cnorm_C0. Qed.
imports: Rlimit Cbase Ctacfield Cnorm Cprop_base Rsequence_def Csequence Csequence_facts Cfunctions