proposition: Lemma egalite_scalaire_deux_projetes : forall A B C H K : PO, A <> B -> A <> C -> H = projete_orthogonal A B C -> K = projete_orthogonal A C B -> scalaire (vec A B) (vec A H) = scalaire (vec A K) (vec A C).
proof: Proof. intros. elim scalaire_deux_projetes with (A := A) (B := B) (C := C) (H := H) (K := K); [ intros H4 H5; try clear scalaire_deux_projetes; try exact H5 | auto | auto | auto | auto ]. rewrite <- H4; auto. Qed.