proposition: Lemma point_contact_cercles_tangents : forall O A O' A' B : PO, O <> A -> O' <> A' -> alignes O B O' -> cercle_rayon O A B -> cercle_rayon O' A' B -> mult_PP (distance O A) (vec O' B) = mult_PP (distance O' A') (vec O B) \/ mult_PP (distance O A) (vec O' B) = mult_PP (- distance O' A') (vec O B).
proof: Proof. icercle. assert (O <> B). apply (isometrie_distinct (A:=O) (B:=A) (A':=O) (B':=B)); auto with geo. cut (alignes B O O'); [ intros H20 | auto with geo ]. halignes H20 k. absurd (B = O); auto. assert (vec O' B = mult_PP k (vec O B)). VReplace (vec O' B) (mult_PP (-1) (vec B O')). rewrite H5; Ringvec. elim (Rlt_le_dec k 0); intros. right; try assumption. apply point_contact_k_negatif with k; auto with real. left; try assumption. apply point_contact_k_positif with k; auto with real. Qed.