proposition: Lemma triangle_hauteurs_secantes : forall A B C H K : PO, triangle A B C -> H = projete_orthogonal A B C -> K = projete_orthogonal A C B -> concours (droite C H) (droite B K).
proof: Proof. intros. deroule_triangle A B C. elim (def_projete_orthogonal2 (A:=A) (B:=B) (C:=C) (H:=H)); auto; intros. elim (def_projete_orthogonal2 (A:=A) (B:=C) (C:=B) (H:=K)); auto; intros. cut (C <> H); intros. cut (B <> K); intros. elim (position_relative_droites_coplanaires (A:=C) (B:=H) (C:=B) (D:=K)); auto with geo; intros. absurd (paralleles (droite C H) (droite B K)); auto. apply angle_non_paralleles; auto. rewrite (angles_droites_orthogonales (A:=A) (B:=C) (C:=A) (D:=B) (E:=B) (F:=K) (G:=C) (I:=H)); auto with geo. apply (triangle_distincts_pied_hauteur (A:=A) (B:=C) (C:=B) (H:=K)); auto with geo. apply (triangle_distincts_pied_hauteur (A:=A) (B:=B) (C:=C) (H:=H)); auto with geo. Qed.