proposition: Theorem 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 C) = scalaire (vec A B) (vec A H) /\ scalaire (vec A B) (vec A C) = scalaire (vec A K) (vec A C).
proof: Proof. intros. elim (def_projete_orthogonal2 (A:=A) (B:=B) (C:=C) (H:=H)); auto; intros. elim (def_projete_orthogonal2 (A:=A) (B:=C) (C:=B) (H:=K)); auto; intros. split; [ try assumption | idtac ]. apply scalaire_avec_projete; auto. rewrite scalaire_sym. rewrite (scalaire_sym A K A C). apply scalaire_avec_projete; auto. Qed.