proposition: Lemma circonscrit_isocele : forall O A B C : PO, circonscrit O A B C -> isocele O B C.
proof: Proof. unfold circonscrit, isocele in |- *; intros; auto. elim H; intros; auto. rewrite <- H0; rewrite <- H1; auto. Qed.