proposition: Lemma Cnorm_triang_rev_l : forall z1 z2 : C, Cnorm z1- Cnorm z2 <= (Cnorm (z1 - z2)).
proof: Proof. intros z1 z2 ; apply Rle_trans with (Rabs (Cnorm z1 - Cnorm z2)) ; [apply RRle_abs | apply Cnorm_triang_rev]. Qed.
imports: Cbase Cpow