proposition: Theorem cercle_neuf_points : forall A B C A' B' C' O G H I J K L H1 H2 H3 : 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 -> K = milieu B H -> L = milieu C H -> H1 = projete_orthogonal B C A -> H2 = projete_orthogonal C A B -> H3 = projete_orthogonal A B C -> (sont_cocycliques A' B' C' J /\ sont_cocycliques A' B' C' H1) /\ (sont_cocycliques A' B' C' K /\ sont_cocycliques A' B' C' H2) /\ sont_cocycliques A' B' C' L /\ sont_cocycliques A' B' C' H3.
proof: Proof. intros. split; [ try assumption | idtac ]. split; [ try assumption | idtac ]. apply (symetrique_milieu_cercle (A:=A) (B:=B) (C:=C) (A':=A') (B':=B') (C':=C') (O:=O) (G:=G) (H:=H) (I:=I)); auto. apply (symetrique_milieu_milieu (A:=A) (B:=B) (C:=C) (A':=A') (B':=B') (C':=C') (O:=O) (G:=G) (H:=H) (I:=I) (J:=J)); auto. Comments Image "file://C:/Documents and Settings/Frédérique Guilhot/.pcoq/figures/f1043314145.gif". apply (pied_hauteur_cercle (A:=A) (B:=B) (C:=C) (A':=A') (B':=B') (C':=C') (O:=O) (G:=G) (H:=H) (I:=I) (J:=J) (HA:=H1)); auto. split; [ split; [ try assumption | idtac ] | idtac ]. cut (sont_cocycliques B' C' A' K); intros; auto with geo. apply (symetrique_milieu_cercle (A:=B) (B:=C) (C:=A) (A':=B') (B':=C') (C':=A') (O:=O) (G:=G) (H:=H) (I:=I)); auto with geo. rewrite H7; apply centre_gravite_ordre_cycle. apply circonscrit_permute; apply circonscrit_permute; auto with geo. apply (symetrique_milieu_milieu (A:=B) (B:=C) (C:=A) (A':=B') (B':=C') (C':=A') (O:=O) (G:=G) (H:=H) (I:=I) (J:=K)); auto with geo. rewrite H7; apply centre_gravite_ordre_cycle. apply circonscrit_permute; apply circonscrit_permute; auto. cut (sont_cocycliques B' C' A' H2); intros; auto with geo. apply (pied_hauteur_cercle (A:=B) (B:=C) (C:=A) (A':=B') (B':=C') (C':=A') (O:=O) (G:=G) (H:=H) (I:=I) (J:=K) (HA:=H2)); auto with geo. rewrite H7; apply centre_gravite_ordre_cycle. apply circonscrit_permute; apply circonscrit_permute; auto. split; [ try assumption | idtac ]. cut (sont_cocycliques C' A' B' L); intros. apply cocycliques_ordre_cycle2; auto. apply (symetrique_milieu_cercle (A:=C) (B:=A) (C:=B) (A':=C') (B':=A') (C':=B') (O:=O) (G:=G) (H:=H) (I:=I) (J:=L)); auto with geo. rewrite H7; apply centre_gravite_ordre_cycle2. apply circonscrit_permute; auto. apply (symetrique_milieu_milieu (A:=C) (B:=A) (C:=B) (A':=C') (B':=A') (C':=B') (O:=O) (G:=G) (H:=H) (I:=I) (J:=L)); auto with geo. rewrite H7; apply centre_gravite_ordre_cycle2. apply circonscrit_permute; auto. cut (sont_cocycliques C' A' B' H3); intros. apply cocycliques_ordre_cycle2; auto with geo. apply (pied_hauteur_cercle (A:=C) (B:=A) (C:=B) (A':=C') (B':=A') (C':=B') (O:=O) (G:=G) (H:=H) (I:=I) (J:=L) (HA:=H3)); auto with geo. rewrite H7; apply centre_gravite_ordre_cycle2. apply circonscrit_permute; auto. Qed.