proposition: Lemma cocyclicite_cercle_diametre : forall A B C D A' : PO, triangle A B C -> sont_cocycliques A B C D -> diametre_circonscrit A A' B C -> diametre_circonscrit A A' C D.
proof: Proof. unfold sont_cocycliques, diametre_circonscrit in |- *; intros. elim H0; [ intros O1 H3; elim H3; [ intros H4 H5; try clear H3 H0; try exact H5 ] ]. elim H1; [ intros O H0; elim H0; [ intros H2 H3; try clear H0 H1; try exact H3 ] ]. assert (O1 = O). apply (unicite_circonscrit_triangle H H4 H3); auto. rewrite H0 in H5; clear H4 H0. exists O. split; [ try assumption | idtac ]. hcercle H3. hcercle H5. Qed.