proposition: Theorem Al_Kashi : forall (A B C : PO) (a : R), A <> B -> A <> C -> image_angle a = cons_AV (vec A B) (vec A C) -> Rsqr (distance B C) = Rsqr (distance A B) + Rsqr (distance A C) + - (2 * (distance A B * (distance A C * cos a))).
proof: Proof. unfold Rsqr in |- *; intros. repeat rewrite <- carre_scalaire_distance. rewrite (difference_Pythagore A B C). rewrite (produit_scalaire_cosinus (A:=A) (B:=B) (C:=C) (a:=a)); auto. ring. Qed.