proposition: Lemma calcul_distance_droite : forall A B C : PO, A <> B -> distance_droite C (droite A B) = Rabs (det (vec A B) (vec A C)) / distance 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 ]. repeat rewrite determinant_aire. rewrite (distance_droite_def (A:=A) (B:=B) (C:=C) (H:=H)); auto. rewrite (aire_avec_projete (A:=A) (B:=B) (C:=C) (H:=H)); auto. replace (distance C H) with (distance H C); auto with geo. elim (def_projete_orthogonal2 (A:=A) (B:=B) (C:=C) (H:=H)); auto; intros. rewrite aire_orthogonal; auto with geo. unfold Rdiv in |- *. cut (distance A B <> 0); intros; auto with geo. RReplace (distance A B * distance H C * / distance A B) (distance A B * / distance A B * distance H C). RReplace (distance A B * / distance A B) 1. ring. Qed.