proposition: Lemma C_dist_tri : forall a b c, C_dist a b <= C_dist a c + C_dist c b.
proof: Proof. intros ; unfold C_dist ; replace (a - b) with ((a - c) + (c - b)) by field ; apply Cnorm_triang. Qed.
imports: Rlimit Cbase Ctacfield Cnorm Cprop_base Rsequence_def Csequence Csequence_facts Cfunctions