proposition: Lemma calcul_Cos_Sin : forall (a b : R) (O I J M : PO), repere_orthonormal_direct O I J -> distance O M = 1 -> vec O M = add_PP (mult_PP a (vec O I)) (mult_PP b (vec O J)) :>PP -> a = Cos (cons_AV (vec O I) (vec O M)) /\ b = Sin (cons_AV (vec O I) (vec O M)).
proof: Proof. intros. elim H; intros. elim H3; intros H4 H5; try clear H3. mesure O I O M. rewrite H3. 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 (calcul_cos_sin (x:=x) (a:=a) (b:=b) (O:=O) (I:=I) (J:=J) (M:=M)); auto. Qed.