proposition: Lemma milieu_sommet_orthocentre_cercle : forall A B C A' B' C' O G H I J : 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 -> sont_cocycliques A' B' C' J.
proof: Proof. intros. apply (symetrique_milieu_cercle (A:=A) (B:=B) (C:=C) (A':=A') (B':=B') (C':=C') (O:=O) (G:=G) (H:=H) (I:=I) (J:=J)); 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. Qed.