proposition: Lemma intersection_deux_hauteurs_orthocentre_triangle : 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 = pt_intersection (droite C H) (droite B K) :>PO -> I = orthocentre A B C :>PO.
proof: Proof. intros A B C H K I H0 H2 H3 H4. 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. cut (~ alignes C H B \/ ~ alignes C H K); intros. elim def_pt_intersection2 with (A := C) (B := H) (C := B) (D := K) (I := I); [ try clear def_pt_intersection2; intros | auto | auto | auto | auto ]. halignes H16 k. halignes H15 k0. cut (orthogonal (vec I B) (vec A C) /\ orthogonal (vec I C) (vec A B)); intros. elim H19; intros H20 H21; try clear H19; try exact H21. apply orthocentre_def; auto. apply deux_hauteurs_trois. auto with geo. auto with geo. split; [ idtac | try assumption ]. replace (vec I B) with (mult_PP (-1) (vec B I)). rewrite H17. replace (mult_PP (-1) (mult_PP k (vec B K))) with (mult_PP k (vec K B)). Simplortho. Ringvec. Ringvec. replace (vec I C) with (mult_PP (-1) (vec C I)). rewrite H18. replace (mult_PP (-1) (mult_PP k0 (vec C H))) with (mult_PP k0 (vec H C)). Simplortho. Ringvec. Ringvec. apply aux with (A := A); auto. 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. Qed.