proposition: Lemma k_negatif_barycentre : 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 -> B = barycentre (cons (distance O A) O') (cons (distance O' A') O).
proof: Proof. intros. assert (mult_PP (distance O A) (vec O' B) = mult_PP (- distance O' A') (vec O B)). apply point_contact_k_negatif 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 (distance O A + distance O' A' <> 0). apply tech_Rplus; auto with geo real. elim H9; intros; auto. absurd (distance O' A' = 0); auto. apply def_vecteur_bary_rec; auto. VReplace (mult_PP (distance O' A') (vec B O)) (mult_PP (- distance O' A') (vec O B)). rewrite <- H5. Ringvec. Qed.