proposition: Lemma unicite_projete_orthogonal : forall A B C H H' : PO, A <> B -> alignes A B H -> orthogonal (vec A B) (vec H C) -> alignes A B H' -> orthogonal (vec A B) (vec H' C) -> H = H'.
proof: Proof. intros. apply scalaire_alignes with (2 := H1) (3 := H3); auto. rewrite <- (scalaire_avec_projete (A:=A) (B:=B) (C:=C) (H:=H)); auto. rewrite <- (scalaire_avec_projete (A:=A) (B:=B) (C:=C) (H:=H')); auto. Qed.