proposition: Lemma circonscrit_permute : forall O A B C : PO, circonscrit O B C A -> circonscrit O A B C.
proof: Proof. unfold circonscrit in |- *; intros. elim H; intros; split; auto with geo. lapply (circonscrit_isocele (O:=O) (A:=B) (B:=C) (C:=A)); auto with geo. Qed.