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