proposition: Lemma cocycliques_existence_diametre : forall A B C D : PO, sont_cocycliques A B C D -> exists A' : PO, diametre_circonscrit A A' B C.
proof: Proof. intros. generalize H; unfold sont_cocycliques, diametre_circonscrit in |- *; intros. elim H0; [ intros O H1; elim H1; [ intros H2 H3; try clear H1 H0; try exact H3 ] ]. symetrique O A A'. exists A'; exists O. tauto. Qed.