proposition: Lemma point_contact_k_negatif : 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 -> mult_PP (distance O A) (vec O' B) = mult_PP (- distance O' A') (vec O B).
proof: Proof. icercle. assert (distance O A <> 0); auto with geo. assert (Rsqr k = Rsqr (distance O' A' * / distance O A)). unfold Rsqr in |- *. assert (O <> B). apply (isometrie_distinct (A:=O) (B:=A) (A':=O) (B':=B)); auto with geo. assert (distance O B <> 0); auto with geo. apply Rmult_eq_reg_l with (scalaire (vec O B) (vec O B)); auto with geo real. replace (scalaire (vec O B) (vec O B) * (k * k)) with (scalaire (mult_PP k (vec O B)) (mult_PP k (vec O B))). rewrite <- H2. repeat rewrite carre_scalaire_distance. rewrite H3; rewrite H4. RReplace (distance O B * distance O B * (distance O' B * / distance O B * (distance O' B * / distance O B))) (distance O' B * distance O' B * (distance O B * / distance O B * (distance O B * / distance O B))). RReplace (distance O B * / distance O B) 1. ring. Simplscal. rewrite H2. assert (- k = distance O' A' * / distance O A). apply Rsqr_inj; auto with real geo. rewrite <- H6; unfold Rsqr in |- *; ring. RReplace k (- - k). rewrite H7. VReplace (mult_PP (distance O A) (mult_PP (- (distance O' A' * / distance O A)) (vec O B))) (mult_PP (- (distance O' A' * (distance O A * / distance O A))) (vec O B)). RReplace (distance O A * / distance O A) 1. Ringvec. Qed.