proposition: Lemma existence_rayon_circonscrit: forall A B C, triangle A B C -> (exists O : PO , circonscrit O A B C /\ (exists r : R , r = distance O C ) ).
proof: Proof. intros. elim existence_cercle_circonscrit with ( A := A ) ( B := B ) ( C := C ); [intros O H0; (try clear existence_cercle_circonscrit); (try exact H0) | auto]. exists O. split; [try assumption | idtac]. exists (distance O C); auto. Qed.