proposition: Lemma passage_polaire_algebrique : forall (z : C) (r a x y : R), z <> zeroC -> z = cons_cart x y -> z = cons_pol r a -> x = r * cos a /\ y = r * sin a.
proof: Proof. intros. elim existence_image_complexe with (z := z); intros M H2; try clear existence_image_complexe; try exact H2. elim coordonnees_polaires_cartesiennes with (x := x) (y := y) (a := a) (r := r) (O := O) (I := I) (J := J) (M := M); [ intros; eauto with geo | eauto with geo | eauto with geo | eauto with geo | eauto with geo | eauto with geo ]. symmetry in |- *; eauto with geo. symmetry in |- *; eauto with geo. Qed.