proposition: Lemma passage_algebrique_argument : forall (z : C) (r x y a : R), z <> zeroC -> z = cons_cart x y -> z = cons_pol r a -> cos a = / r * x /\ sin a = / r * y.
proof: Proof. intros. elim passage_polaire_algebrique with (z := z) (r := r) (a := a) (x := x) (y := y); [ intros | eauto with geo | eauto with geo | eauto with geo ]. cut (r <> 0); intros. split; [ try assumption | idtac ]. rewrite H2. field; auto. rewrite H3. field; auto. replace r with (module z); eauto with geo. Qed.