proposition: Lemma coordonnees_Cos_Sin : forall O I J M : PO, repere_orthonormal_direct O I J -> distance O M = 1 -> vec O M = add_PP (mult_PP (Cos (cons_AV (vec O I) (vec O M))) (vec O I)) (mult_PP (Sin (cons_AV (vec O I) (vec O M))) (vec O J)) :>PP.
proof: Proof. intros. elim H; intros. elim H2; intros H4 H5; try clear H2. mesure O I O M. rewrite H2. rewrite <- (trivial_sin_Sin (A:=O) (B:=I) (C:=M) (D:=J) (x:=x)); auto with geo. rewrite <- (trivial_cos_Cos (A:=O) (B:=I) (C:=M) (x:=x)); auto with geo. apply coordonnees_cos_sin; auto. Qed.