proposition: Lemma existence_rayon_diametre : forall A B O : PO, cercle_rayon O A B -> exists C : PO, cercle_diametre A C B.
proof: Proof. unfold cercle_rayon, isocele in |- *; intros. symetrique O A M. exists M. icercle. exists O. auto with geo. Qed.