proposition: Lemma cercles_tangents_tangente_commune : forall O A O' A' : PO, O <> A -> O' <> A' -> cercles_tangents O A O' A' -> exists B : PO, (exists M : PO, B <> M /\ tangente_cercle O A B M /\ tangente_cercle O' A' B M).
proof: Proof. unfold cercles_tangents, tangente_cercle in |- *; intros. 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 ]. assert (O <> B). hcercle H5. apply (isometrie_distinct (A:=O) (B:=A) (A':=O) (B':=B)); auto with geo. soit_orthogonal B O M. exists B; exists M. split; [ auto | split; [ split; [ try assumption | auto with geo ] | try assumption ] ]. split; [ try assumption | idtac ]. halignes H3 k. apply ortho_sym. VReplace (vec B O') (add_PP (vec B O) (vec O O')). rewrite H7. VReplace (add_PP (vec B O) (mult_PP k (vec O B))) (mult_PP (- k + 1) (vec B O)). auto with geo. Qed.