proposition: Lemma C_dist_pos : forall a b, C_dist a b >= 0.
proof: Proof. intros ; unfold C_dist ; apply Rle_ge ; apply Cnorm_pos. Qed.
imports: Rlimit Cbase Ctacfield Cnorm Cprop_base Rsequence_def Csequence Csequence_facts Cfunctions