proposition: Lemma cercle_diametre_degenere : forall A B M : PO, A = B -> cercle_diametre A B M -> A = M.
proof: Proof. intros A B M H; try assumption. rewrite H; icercle. elim H0; [ intros O' H1; elim H1; [ intros H2 H3; elim H2; [ intros H4 H5; try clear H2 H1 H0; try exact H5 ] ] ]. assert (O' = B). rewrite (milieu_trivial B); auto. rewrite <- H0. apply distance_refl1. rewrite <- H5; rewrite <- H0; auto with geo. Qed.