proposition: Lemma diametre_circonscrit_centre : forall A B C A' O : PO, triangle A B C -> circonscrit O A B C -> diametre_circonscrit A A' B C -> cercle_diametre A A' B.
proof: Proof. unfold sont_cocycliques, diametre_circonscrit in |- *; intros. elim H1; [ intros O1 H2; elim H2; [ intros H3 H4; try clear H2 H1; try exact H4 ] ]. assert (O1 = O). apply (unicite_circonscrit_triangle H H4 H0); auto. rewrite H1 in H3; clear H4 H1. apply circonscrit_diametre with (C := C) (O := O); auto. Qed.