proposition: Lemma cercles_concentriques_tangents_egaux : forall O A A' : PO, O <> A -> O <> A' -> cercles_tangents O A O A' -> cercle_rayon O A A'.
proof: Proof. unfold cercles_tangents in |- *; icercle. elim H1; [ intros B H2; elim H2; [ intros H3 H4; elim H4; [ intros H5 H6; try clear H4 H2 H1; try exact H5 ] ] | auto | auto ]. rewrite H6; auto. Qed.