proposition: Lemma k_positif_distance_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 -> distance O O' = Rabs (distance O A + - distance O' A').
proof: Proof. intros. assert (distance O A <> 0); auto with geo. assert (vec O O' = mult_PP (/ distance O A * (distance O A + - distance O' A')) (vec O B)). apply k_positif_vecteur_centres with k; auto. rewrite (colinearite_distance H6). rewrite Rabs_mult. rewrite Rabs_right; auto with real geo. hcercle H3. rewrite <- H7. RReplace (/ distance O A * Rabs (distance O A + - distance O' A') * distance O A) (/ distance O A * distance O A * Rabs (distance O A + - distance O' A')). RReplace (/ distance O A * distance O A) 1. ring. Qed.