proposition: Lemma produit_scalaire_cosinus : forall (A B C : PO) (a : R), A <> B -> A <> C -> image_angle a = cons_AV (vec A B) (vec A C) -> scalaire (vec A B) (vec A C) = distance A B * (distance A C * cos a).
proof: Proof. intros. rewrite produit_scalaire_Cosinus; auto. rewrite (egalite_cos_Cos (A:=A) (B:=B) (C:=C) (x:=a)); auto. Qed.