proposition: Lemma coordonnees_cos_sin : forall (x : R) (O I J M : PO), repere_orthonormal_direct O I J -> image_angle x = cons_AV (vec O I) (vec O M) -> distance O M = 1 -> vec O M = add_PP (mult_PP (cos x) (vec O I)) (mult_PP (sin x) (vec O J)) :>PP.
proof: Proof. intros. elim H; intros. elim H3; intros H4 H5; try clear H3; try exact H5. rewrite (def_sin (A:=O) (B:=I) (C:=M) (D:=J) (x:=x)); auto with geo. rewrite (def_cos (A:=O) (B:=I) (C:=M) (x:=x)); auto with geo. pattern (vec O M) at 1 in |- *. rewrite (coordonnees_scalaire_base (O:=O) (I:=I) (J:=J) M); auto with geo. rewrite scalaire_sym; auto. Qed.