proposition: Lemma scalaire_avec_projete : forall A B C H : PO, alignes A B H -> orthogonal (vec A B) (vec H C) -> scalaire (vec A B) (vec A C) = scalaire (vec A B) (vec A H).
proof: Proof. intros. discrimine A B. VReplace (vec B B) (mult_PP 0 (vec B C)). Simplscal. halignes H0 k. replace (vec A C) with (add_PP (vec A H) (vec H C)). Simplscal. replace (scalaire (vec A B) (vec H C)) with 0. ring. symmetry in |- *. apply def_orthogonal; auto. Ringvec. Qed.