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