proposition: Lemma k_positif_vecteur_centres : forall (O A O' A' B : PO) (k : R), k >= 0 -> O <> A -> O' <> A' -> vec O' B = mult_PP k (vec O B) -> cercle_rayon O A B -> cercle_rayon O' A' B -> vec O O' = mult_PP (/ distance O A * (distance O A + - distance O' A')) (vec O B).
proof: Proof. intros. assert (mult_PP (distance O A) (vec O' B) = mult_PP (distance O' A') (vec O B)). apply point_contact_k_positif with k; auto. assert (distance O A <> 0); auto with geo. assert (distance O' A' <> 0); auto with geo. assert (distance O A >= 0); auto with geo. assert (distance O' A' >= 0); auto with geo. assert (mult_PP (distance O A + - distance O' A') (vec O B) = mult_PP (distance O A) (vec O O')). VReplace (mult_PP (distance O A) (vec O O')) (add_PP (mult_PP (distance O A) (vec O B)) (mult_PP (-1) (mult_PP (distance O A) (vec O' B)))). rewrite H5. Ringvec. VReplace (mult_PP (/ distance O A * (distance O A + - distance O' A')) (vec O B)) (mult_PP (/ distance O A) (mult_PP (distance O A + - distance O' A') (vec O B))). rewrite H10. VReplace (mult_PP (/ distance O A) (mult_PP (distance O A) (vec O O'))) (mult_PP (distance O A * / distance O A) (vec O O')). RReplace (distance O A * / distance O A) 1. Ringvec. Qed.