proposition: Lemma aux : 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 -> ~ alignes C H B \/ ~ alignes C H 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 (classic (orthogonal (vec B A) (vec B C))); intros. cut (H = B); intros. right; try assumption. rewrite H14. cut (~ orthogonal (vec A C) (vec B C)); intros. red in |- *; intros; apply H15. assert (alignes B K C); auto with geo. halignes H17 k. apply ortho_sym. rewrite H18. Simplortho. elim triangle_rectangle_une_fois with (A := B) (B := A) (C := C); [ try clear triangle_rectangle_une_fois; intros | auto with geo | auto ]. red in |- *; intros; apply H16. auto with geo. apply unicite_projete_orthogonal with (2 := H7) (3 := H8); auto with geo. left. red in |- *; intros; apply H13. halignes H14 k. apply ortho_sym. replace (vec B C) with (mult_PP (-1) (vec C B)); [ idtac | Ringvec ]. rewrite H15. replace (mult_PP (-1) (mult_PP k (vec C H))) with (mult_PP k (vec H C)); [ idtac | Ringvec ]. Simplortho. 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.