proposition: Lemma circonscrit_trans : forall O A B C D : PO, circonscrit O A B C -> circonscrit O A B D -> circonscrit O A C D.
proof: Proof. unfold circonscrit, isocele in |- *; intros. elim H0; clear H0; intros. elim H; clear H; intros. split; auto. Qed.