proposition: Lemma circonscrit_distinct1 : forall O A B C : PO, O <> A -> circonscrit O A B C -> O <> B.
proof: Proof. unfold circonscrit, isocele in |- *; intros. elim H0; [ intros H1 H2; try clear H0; try exact H2 ]. apply isometrie_distinct with (2 := H1); auto. Qed.