proposition: Lemma existence_intersection_deux_hauteurs_triangle : forall A B C H K : PO, triangle A B C -> H = projete_orthogonal A B C :>PO -> K = projete_orthogonal A C B :>PO -> ex (fun I : PO => I = pt_intersection (droite C H) (droite B K) :>PO).
proof: Proof. intros. cut (~ alignes C H B \/ ~ alignes C H K); intros. apply existence_pt_intersection; auto. apply (triangle_distincts_pied_hauteur (A:=A) (B:=B) (C:=C) (H:=H)); auto. apply (triangle_distincts_pied_hauteur (A:=A) (B:=C) (C:=B) (H:=K)); auto with geo. apply triangle_hauteurs_secantes with (A := A); auto. apply aux with (A := A); auto. Qed.