proposition: Lemma circonscrit_mediatrice : forall O A B C : PO, circonscrit O A B C -> mediatrice A B O /\ mediatrice B C O /\ mediatrice A C O.
proof: Proof. unfold circonscrit, isocele, mediatrice in |- *; intros; auto. elim H; intros; auto. split; [ assumption | split; [ idtac | try assumption ] ]. rewrite <- H0; auto. Qed.