proposition: Lemma orthocentre_intersection_hauteurs : forall A B C H K I : PO, triangle A B C -> H = projete_orthogonal A B C :>PO -> K = projete_orthogonal A C B :>PO -> I = orthocentre A B C :>PO -> I = pt_intersection (droite C H) (droite B K) :>PO.
proof: Proof. intros. elim orthocentre_def2 with (A := A) (B := B) (C := C) (H := I); [ intros | auto ]. elim H4; intros H6 H7; try clear H4; try exact H7. cut (~ alignes C H B \/ ~ alignes C H K); 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. apply def_pt_intersection; auto. elim orthogonal_colineaires with (A := A) (B := B) (C := H) (D := C) (E := C) (F := I); [ intros k H18; try exact H18 | auto with geo | auto with geo | auto with geo | auto with geo ]. apply colineaire_alignes with (- k); auto. rewrite H18; Ringvec. elim orthogonal_colineaires with (A := A) (B := C) (C := K) (D := B) (E := B) (F := I); [ intros k H18; try exact H18 | auto with geo | auto with geo | auto with geo | auto with geo ]. apply colineaire_alignes with (- k); auto. rewrite H18; Ringvec. 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. apply aux with (A := A); auto. Qed.