proposition: Lemma Cnorm_triang_rev : forall z1 z2 : C, Rabs (Cnorm z1- Cnorm z2) <= (Cnorm (z1 - z2)).
proof: Proof. intros z1 z2. assert (H1 : Cnorm (z1 - z2 + z2) <= (Cnorm (z1 - z2)) + Cnorm z2) by (apply Cnorm_triang). assert (H2 : Cnorm (z2 - z1 + z1) <= (Cnorm (z2 - z1)) + Cnorm z1) by (apply Cnorm_triang). assert (H3 : forall a b, a = a - b + b). CusingR_f. unfold Rabs ; case Rcase_abs ; intro H ; ring_simplify. rewrite <- H3 in H2 ; apply Rminus_le ; apply Rle_minus in H2 ; ring_simplify in H2 ; rewrite Cnorm_minus_sym ; replace ( -Cnorm z1 + Cnorm z2 - Cnorm (z2 - z1))%R with (Cnorm z2 - Cnorm (z2 - z1) - Cnorm z1)%R by field ; apply H2. rewrite <- H3 in H1 ; apply Rminus_le ; apply Rle_minus in H1. replace (Cnorm z1 - Cnorm z2 - Cnorm (z1 - z2))%R with (Cnorm z1 - (Cnorm(z1 - z2) + Cnorm z2))%R by field ; apply H1. Qed.
imports: Cbase Cpow