proposition: Lemma calcul_cos_sin : forall (x a b : 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 a (vec O I)) (mult_PP b (vec O J)) :>PP -> a = cos x /\ b = sin x.
proof: Proof. intros. apply unicite_coordonnees with (2 := H2); auto with geo. apply coordonnees_cos_sin; auto. Qed.