proposition: Lemma circonscrit_diametre : forall A B C D O : PO, circonscrit O A B C -> O = milieu A D -> cercle_diametre A D B.
proof: Proof. icercle. exists O. split; [ split; [ auto with geo | try assumption ] | try assumption ]. Qed.