proposition: Lemma changement_diametre : forall A B C D C' O : PO, triangle A B C -> circonscrit O A B C -> O = milieu C C' -> sont_cocycliques A B C D -> cercle_diametre C C' D.
proof: Proof. unfold cercle_diametre, sont_cocycliques in |- *; intros. elim H2; [ intros O1 H3; elim H3; [ intros H4 H5; try clear H3 H2; try exact H5 ] ]. assert (O1 = O). apply (unicite_circonscrit_triangle H H4 H0); auto. rewrite H2 in H5; clear H4 H2. hcercle H5; hcercle H0. exists O. icercle. icercle. rewrite <- H7; auto. Qed.