proposition: Lemma coordonnees_polaires_cartesiennes : forall (x y a r : R) (O I J M : PO), repere_orthonormal_direct O I J -> O <> M -> r = distance O M -> image_angle a = cons_AV (vec O I) (vec O M) -> vec O M = add_PP (mult_PP x (vec O I)) (mult_PP y (vec O J)) :>PP -> x = r * cos a /\ y = r * sin a.
proof: Proof. intros. apply unicite_coordonnees with (2 := H3); auto with geo. elim existence_representant_unitaire with (A := O) (B := M); [ intros C H4; try clear existence_unitaire; try exact H4 | auto ]. rewrite (distance_vecteur (A:=O) (B:=M)); auto. rewrite <- H4. rewrite (coordonnees_cos_sin (x:=a) (O:=O) (I:=I) (J:=J) (M:=C)); auto. rewrite <- H1. unfold vec in |- *; RingPP. rewrite H2. rewrite H4. inversion H. elim H6; intros H7 H8; try clear H6; try exact H7. rewrite angles_representants_unitaires; auto with geo. replace (representant_unitaire (vec O I)) with (vec O I); auto with geo. elim def_representant_unitaire2 with (A := O) (B := M) (C := C); [ intros; elim H6; intros H7 H8; try clear H6 def_representant_unitaire2; auto with geo | auto | auto ]. Qed.