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