proposition: Lemma polaire_calcul_algebrique : forall (z : C) (r a : R), z <> zeroC :>C -> z = cons_pol r a :>C -> z = cons_cart (r * cos a) (r * sin a) :>C.
proof: Proof. intros. elim existence_parties_relles_imaginaires with (z := z); intros a0 H1; elim H1; intros b H2; try clear H1 existence_parties_relles_imaginaires; try exact H2. elim passage_polaire_algebrique with (z := z) (r := r) (a := a) (x := a0) (y := b); [ intros; try exact H4 | auto | auto | auto ]. rewrite H2; rewrite H3; rewrite H4; auto. Qed.