proposition: Lemma symetrique_milieu_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 = symetrie I A' -> sont_cocycliques A' B' C' J.
proof: Proof. unfold symetrie in |- *; intros. unfold sont_cocycliques, circonscrit, isocele in |- *. exists I. cut (circonscrit I A' B' C'); intros. 2: apply (centre_circonscrit_triangle_homothetique (A:=A) (B:=B) (C:=C) (A':=A') (B':=B') (C':=C') (O:=O) (G:=G) (H:=H) (I:=I)); auto. generalize H9; unfold circonscrit, isocele in |- *; intros. split; [ try assumption | idtac ]. elim H10; intros H11 H12; try clear H10; try exact H11. split; [ try assumption | idtac ]. apply carre_scalaire_egalite_distance. rewrite (homothetie_vecteur (k:=-1) (I:=I) (A:=A') (A':=J)); auto. Simplscal. Qed.