proposition: Lemma tangente_commune_cercles_tangents : forall O A O' A' B M : PO, O <> A -> O' <> A' -> B <> M -> tangente_cercle O A B M -> tangente_cercle O' A' B M -> cercles_tangents O A O' A'.
proof: Proof. unfold cercles_tangents, tangente_cercle in |- *; intros. repeat applatit_and. exists B. split; [ idtac | split; try assumption ]. assert (O <> B). hcercle H3. apply (isometrie_distinct (A:=O) (B:=A) (A':=O) (B':=B)); auto with geo. elim orthogonal_colineaires with (A := B) (B := M) (C := B) (D := O) (E := B) (F := O'); [ intros | auto | auto | auto | auto ]. apply colineaire_alignes with (- x + 1). VReplace (vec O O') (add_PP (vec O B) (vec B O')). rewrite H9. VReplace (add_PP (vec O B) (mult_PP x (vec B O))) (mult_PP (- x + 1) (vec O B)); auto. Qed.