proposition: Lemma triangle_intersection_mediatrices : forall A B C B' C' O : PO, triangle A B C -> C' <> O -> B' <> O -> C' = milieu A B -> B' = milieu A C -> circonscrit O A B C -> ~ alignes C' O B'.
proof: Proof. unfold circonscrit, isocele in |- *; intros. deroule_triangle A B C. cut (~ paralleles (droite C' O) (droite B' O)); intros. red in |- *; intros; apply H9. rewrite droite_permute; auto. rewrite (droite_permute (A:=B') (B:=O)); auto. apply alignes_paralleles; auto with geo. apply angle_non_paralleles; auto. elim H4; intros H10 H11; try clear H4; try exact H11. rewrite (angles_droites_orthogonales (A:=A) (B:=C) (C:=A) (D:=B) (E:=B') (F:=O) (G:=C') (I:=O)); auto with geo. apply ortho_sym. apply mediatrice_orthogonale_segment; auto. apply milieu_mediatrice; auto. apply ortho_sym. apply mediatrice_orthogonale_segment; auto. apply milieu_mediatrice; auto. Qed.