proposition: Lemma scalaire_composantes_ABCD : forall (O I J A B C D : PO) (x y x' y' : R), repere_orthonormal O I J -> vec A B = add_PP (mult_PP x (vec O I)) (mult_PP y (vec O J)) -> vec C D = add_PP (mult_PP x' (vec O I)) (mult_PP y' (vec O J)) -> scalaire (vec A B) (vec C D) = x * x' + y * y'.
proof: Proof. intros. elim existence_representant_vecteur with (A := O) (B := A) (C := B); [ intros M H20 ]. elim existence_representant_vecteur with (A := O) (B := C) (C := D); [ intros N H21 ]. rewrite <- H20; rewrite <- H21. rewrite (scalaire_coordonnees (O:=O) (I:=I) (J:=J) (M:=M) (N:=N) (x:=x) (y:=y) (x':=x') (y':=y')); auto with geo. rewrite H20; auto. rewrite H21; auto. Qed.