proposition: Lemma existence_distance_droite : forall A B C : PO, A <> B -> exists d : R, d = distance_droite C (droite A B).
proof: Proof. intros A B C H0; try assumption. elim existence_projete_orthogonal with (A := A) (B := B) (C := C); [ intros H H1; try clear existence_projete_orthogonal; try exact H1 | auto ]. exists (distance C H). rewrite (distance_droite_def (A:=A) (B:=B) (C:=C) (H:=H)); auto. Qed.