proposition: Lemma existence_cercle_circonscrit_diametre : forall A B C : PO, triangle A B C -> exists O : PO, (exists D : PO, circonscrit O A B C /\ cercle_diametre A D C /\ sont_cocycliques A B C D).
proof: Proof. intros. elim existence_cercle_circonscrit with (A := A) (B := B) (C := C); [ unfold circonscrit, isocele in |- *; intros O H0; try exact H0 | auto ]. exists O. symetrique O A D. exists D. split; [ try assumption | idtac ]. applatit_and. icercle. exists O. icercle. exists O. icercle. Qed.