proposition: Lemma cercle_diametre_trivial2 : forall A B : PO, cercle_diametre A B B.
proof: Proof. icercle. discrimine A B. exists B; split; auto with geo. soit_milieu A B M. exists M. split; auto. split; auto with geo. Qed.