proposition: Theorem existence_cercle_circonscrit : forall A B C : PO, triangle A B C -> ex (fun O : PO => circonscrit O A B C).
proof: Proof. intros. deroule_triangle A B C. soit_mediatrice A B M K. soit_mediatrice B C J L. lapply (mediatrices_triangle_concours (A:=A) (B:=B) (C:=C) (I:=M) (J:=J) (K:=K) (L:=L)); auto; intros. elim (def_concours2 (A:=M) (B:=K) (C:=J) (D:=L)); auto; intros. exists x. apply circonscrit_permute. unfold circonscrit in |- *. elim H19; clear H19; intros. split; apply mediatrice_isocele. discrimine J x. apply milieu_mediatrice; auto. apply orthogonale_segment_milieu_mediatrice with J; auto. apply ortho_sym; auto. apply paralleles_orthogonal with (A := J) (B := L); auto. apply alignes_paralleles; auto. apply mediatrice_orthogonale_segment; auto. apply milieu_mediatrice; auto. discrimine M x. apply mediatrice_permute. apply milieu_mediatrice; auto. apply mediatrice_permute. apply orthogonale_segment_milieu_mediatrice with M; auto. apply ortho_sym; auto. apply paralleles_orthogonal with (A := M) (B := K); auto. apply alignes_paralleles; auto. apply mediatrice_orthogonale_segment; auto. apply milieu_mediatrice; auto. Qed.