proposition: Lemma centre_circonscrit_triangle_homothetique : forall A B C A' B' C' O G H I : 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 -> circonscrit I A' B' C'.
proof: Proof. intros. generalize H5; unfold circonscrit, isocele in |- *; intros. elim H8; intros H9 H10; try clear H8; try exact H10. split; apply carre_scalaire_egalite_distance. rewrite (homothetie_bipoint (k:=- / 2) (I:=G) (A:=O) (B:=A) (A':=I) (B':=A')); auto. Simplscal. rewrite (homothetie_bipoint (k:=- / 2) (I:=G) (A:=O) (B:=B) (A':=I) (B':=B')); auto. Simplscal. repeat rewrite carre_scalaire_distance. rewrite H9; ring. apply (homothetique_centre_circonscrit (A:=A) (B:=B) (C:=C) (O:=O) (G:=G) (H:=H) (I:=I)); auto. apply centre_gravite_homothetie with (1 := H2); auto. rewrite H4. rewrite centre_gravite_ordre_permute. rewrite centre_gravite_ordre_cycle2; auto. apply (homothetique_centre_circonscrit (A:=A) (B:=B) (C:=C) (O:=O) (G:=G) (H:=H) (I:=I)); auto. apply centre_gravite_homothetie with (1 := H1); auto. rewrite (homothetie_bipoint (k:=- / 2) (I:=G) (A:=O) (B:=A) (A':=I) (B':=A')); auto. Simplscal. rewrite (homothetie_bipoint (k:=- / 2) (I:=G) (A:=O) (B:=C) (A':=I) (B':=C')); auto. Simplscal. repeat rewrite carre_scalaire_distance. rewrite H10; ring. apply (homothetique_centre_circonscrit (A:=A) (B:=B) (C:=C) (O:=O) (G:=G) (H:=H) (I:=I)); auto. apply centre_gravite_homothetie with (1 := H3); auto. rewrite H4. rewrite centre_gravite_ordre_cycle2; auto. apply (homothetique_centre_circonscrit (A:=A) (B:=B) (C:=C) (O:=O) (G:=G) (H:=H) (I:=I)); auto. apply centre_gravite_homothetie with (1 := H1); auto. Qed.