proposition: Lemma cercle_diametre_permute : forall A B C : PO, cercle_diametre A B C -> cercle_diametre B A C.
proof: Proof. icercle. elim H; [ intros O H0; elim H0; [ intros H1 H2; elim H1; [ intros H3 H4; try clear H1 H0 H; try exact H4 ] ] ]. exists O; split; auto with geo. split; [ auto | idtac ]. rewrite <- H3; auto. Qed.