proposition: Lemma existence_perpendiculaire : forall A B C : PO, A <> B -> exists D : PO, orthogonal (vec A B) (vec C D).
proof: Proof. intros A B C H0; try assumption. soit_projete A B C H. exists H. auto with geo. Qed.