proposition: Lemma produit_scalaire_Cosinus : forall A B C : PO, A <> B -> A <> C -> scalaire (vec A B) (vec A C) = distance A B * (distance A C * Cos (cons_AV (vec A B) (vec A C))).
proof: Proof. intros. elim existence_representant_unitaire with (A := A) (B := B); [ intros B' H2; try clear existence_representant_unitaire; try exact H2 | auto ]. elim existence_representant_unitaire with (A := A) (B := C); [ intros C' H3; try clear existence_representant_unitaire; try exact H3 | auto ]. elim existence_ROND_AB with (A := A) (B := B'); [ intros D H10 | auto ]. elim H10; intros. elim H4; intros H6 H7; try clear H4; try exact H7. rewrite angles_representants_unitaires; auto with geo. pattern (vec A B) at 1 in |- *. rewrite distance_vecteur; auto. pattern (vec A C) at 1 in |- *. rewrite distance_vecteur; auto. rewrite <- H3; rewrite <- H2. pattern (vec A C') at 1 in |- *. rewrite (coordonnees_Cos_Sin (O:=A) (I:=B') (J:=D) (M:=C')); auto. replace (mult_PP (distance A C) (add_PP (mult_PP (Cos (cons_AV (vec A B') (vec A C'))) (vec A B')) (mult_PP (Sin (cons_AV (vec A B') (vec A C'))) (vec A D)))) with (add_PP (mult_PP (distance A C * Cos (cons_AV (vec A B') (vec A C'))) (vec A B')) (mult_PP (distance A C * Sin (cons_AV (vec A B') (vec A C'))) (vec A D))). replace (mult_PP (distance A B) (vec A B')) with (add_PP (mult_PP (distance A B) (vec A B')) (mult_PP 0 (vec A D))). Simplscal. replace (scalaire (vec A B') (vec A D)) with 0. rewrite H6; ring. symmetry in |- *; auto with geo. Ringvec. Ringvec. elim def_representant_unitaire2 with (A := A) (B := C) (C := C'); auto with geo; intros. elim H5; auto with geo. elim def_representant_unitaire2 with (A := A) (B := B) (C := B'); auto; intros. elim H4; auto with geo. Qed.