proposition: Lemma pied_hauteur_cercle : forall A B C A' B' C' O G H I J HA : PO, triangle A B C -> A' = milieu B C -> B' = milieu A C -> C' = milieu A B -> G = centre_gravite A B C -> circonscrit O A B C -> H = orthocentre A B C -> I = milieu O H -> J = milieu A H -> HA = projete_orthogonal B C A -> sont_cocycliques A' B' C' HA.
proof: Proof. intros. generalize (orthogonal_diametre_cercle (A:=A') (B:=B') (C:=C') (A':=J) (O:=I)); intros H14; apply H14. apply triangle_triangle_milieux with (1 := H0); auto with geo. generalize (centre_circonscrit_triangle_homothetique (A:=A) (B:=B) (C:=C) (A':=A') (B':=B') (C':=C') (O:=O) (G:=G) (H:=H)); intros H19; apply H19; auto. apply symetrie_milieu. generalize (symetrique_milieu_milieu (A:=A) (B:=B) (C:=C) (A':=A') (B':=B') (C':=C') (O:=O) (G:=G) (H:=H)); intros H19; apply H19; auto. deroule_triangle A B C. elim def_projete_orthogonal2 with (A := B) (B := C) (C := A) (H := HA); [ intros | auto | auto ]. halignes H15 k. cut (alignes B C A'); intros; auto with geo. halignes H18 k0. cut (orthogonal (vec B C) (vec HA J)); intros. replace (vec HA A') with (add_PP (vec B A') (mult_PP (-1) (vec B HA))); [ idtac | Ringvec ]. rewrite H19; rewrite H17. replace (mult_PP (-1) (mult_PP k (vec B C))) with (mult_PP (- k) (vec B C)); [ idtac | Ringvec ]. Simplortho. apply ortho_sym. cut (alignes A H J); intros; auto with geo. cut (alignes A HA H); intros. halignes H20 x. assert (J = A). rewrite H8; rewrite <- H20; auto with geo. rewrite H22; auto with geo. halignes H21 y. absurd (A = HA); auto. red in |- *; intros; apply H10. rewrite H21; auto with geo. replace (vec HA J) with (add_PP (vec HA A) (vec A J)); [ idtac | Ringvec ]. rewrite H22; rewrite H23. replace (add_PP (vec HA A) (mult_PP x (mult_PP y (vec A HA)))) with (mult_PP (1 + - (x * y)) (vec HA A)); [ idtac | Ringvec ]. Simplortho. elim orthocentre_def2 with (A := A) (B := B) (C := C) (H := H); [ intros; elim H21; intros H23 H24; try clear H21 orthocentre_def2; try exact H24 | auto ]. discrimine H A. elim orthogonal_colineaires with (A := B) (B := C) (C := H) (D := A) (E := HA) (F := A); [ intros k1 H26; try clear orthogonal_colineaires | auto with geo | auto with geo | auto with geo | auto with geo ]. cut (alignes A H HA); intros. apply alignes_ordre_permute; try trivial. apply colineaire_alignes with k1. replace (vec A HA) with (mult_PP (-1) (vec HA A)); [ idtac | Ringvec ]. rewrite H26; Ringvec. Qed.