proposition: Theorem cos_diff : forall a b : R, cos (a + - b) = cos a * cos b + sin a * sin b.
proof: Proof. intros. elim existence_AB_unitaire; intros A H; elim H; intros B H0; try clear H; try exact H0. elim existence_ROND_AB with (A := A) (B := B); [ intros D H10 | auto ]. elim existence_representant_angle with (A := A) (B := B) (C := A) (x := a); [ intros C H; elim H; intros H1 H2; try clear H; try exact H2 | auto ]. elim existence_representant_angle with (A := A) (B := B) (C := A) (x := b); [ intros E H; elim H; intros H3 H4; try clear H; try exact H4 | auto ]. generalize (coordonnees_cos_sin (x:=a) (O:=A) (I:=B) (J:=D) (M:=C)); intros H. generalize (coordonnees_cos_sin (x:=b) (O:=A) (I:=B) (J:=D) (M:=E)); intros. replace (cos a * cos b + sin a * sin b) with (scalaire (vec A C) (vec A E)). cut (image_angle (a + - b) = cons_AV (vec A E) (vec A C)); intros. rewrite (def_cos (A:=A) (B:=E) (C:=C) (x:=a + - b)); auto. rewrite scalaire_sym; auto. replace (cons_AV (vec A E) (vec A C)) with (plus (cons_AV (vec A E) (vec A B)) (cons_AV (vec A B) (vec A C))). replace (cons_AV (vec A E) (vec A B)) with (image_angle (- b)). rewrite <- H2. replace (a + - b) with (- b + a). apply add_mes_compatible. ring. apply mes_oppx; auto with geo. apply Chasles; auto with geo. rewrite H5; auto. rewrite H; auto. Simplscal. elim H10; intros. elim H7; intros H8 H9; try clear H7; try exact H9. cut (scalaire (vec A B) (vec A D) = 0); auto with geo; intros. rewrite H9; rewrite H8; rewrite H7. rewrite scalaire_sym; rewrite H7. ring. Qed.