proposition: Lemma existence_argument : forall z : C, z <> zeroC -> exists a : R, argument z = image_angle a.
proof: Proof. intros. elim existence_image_complexe with (z := z); intros M H1; try clear existence_image_complexe; try exact H1. cut (O <> M); intros; eauto with geo. mesure O I O M. exists x. rewrite H2; eauto with geo. Qed.