proposition: Lemma k_negatif_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' = distance O A + distance O' A'.
proof: Proof. intros. 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 (distance O A + distance O' A' <> 0). apply tech_Rplus; auto with geo real. elim H8; intros; auto. absurd (distance O' A' = 0); auto. assert (B = barycentre (cons (distance O A) O') (cons (distance O' A') O)). apply k_negatif_barycentre with k; auto. assert (mult_PP (distance O A + distance O' A') (vec O B) = mult_PP (distance O A) (vec O O')). rewrite <- (prop_vecteur_bary (a:=distance O A) (b:=distance O' A') (A:=O') (B:=O) (G:=B) O); auto. Ringvec. assert (vec O O' = mult_PP (/ distance O A * (distance O A + distance O' A')) (vec O B)). 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 H11. 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. rewrite (colinearite_distance H12). rewrite Rabs_right; auto with real. hcercle H3. rewrite <- H13. RReplace (/ distance O A * (distance O A + distance O' A') * distance O A) (/ distance O A * distance O A * (distance O A + distance O' A')). RReplace (/ distance O A * distance O A) 1. ring. apply Rmult_pos; auto with real geo. lra. Qed.