proposition: Lemma circonscrit_triangle_non_point : forall O A B C : PO, triangle A B C -> circonscrit O A B C -> O <> A /\ O <> B /\ O <> C.
proof: Proof. intros. cut (O <> A); intros. split; [ try assumption | idtac ]. split; [ try assumption | idtac ]. apply circonscrit_distinct1 with (2 := H0); auto. apply circonscrit_distinct2 with (2 := H0); auto. hcercle H0. deroule_triangle A B C. red in |- *; intros. apply H6. rewrite <- H7. assert (distance O B = 0); auto with geo. rewrite <- H2. rewrite <- H7; auto with geo. Qed.