proposition: Lemma existence_forme_polaire : forall z : C, z <> zeroC -> exists r : R, (exists a : R, module z = r /\ argument z = image_angle a).
proof: Proof. intros. elim existence_module with (z := z); intros r H0; try clear existence_module; try exact H0. elim existence_argument with (z := z); [ intros a H1; try clear existence_argument; try exact H1 | auto ]. exists r; exists a; auto. Qed.