proposition: Lemma circonscrit_distinct3 : forall O A B C : PO, O <> B -> circonscrit O A B C -> O <> A.
proof: Proof. intros. assert (circonscrit O B C A). apply circonscrit_permute. apply circonscrit_permute; auto. apply circonscrit_distinct2 with (2 := H1); auto. Qed.