proposition: Theorem cercles_tangents_contact_unique : forall O A O' A' B C : PO, O <> A -> O' <> A' -> ~ cercle_rayon O A A' -> alignes O B O' -> cercle_rayon O A B -> cercle_rayon O' A' B -> alignes O C O' -> cercle_rayon O A C -> cercle_rayon O' A' C -> B = C.
proof: Proof. intros O A O' A' B C H H0 H100 H1 H2 H3 H4 H5 H6; try assumption. assert (O <> B). apply (isometrie_distinct (A:=O) (B:=A) (A':=O) (B':=B)); auto with geo. assert (O <> C). apply (isometrie_distinct (A:=O) (B:=A) (A':=O) (B':=C)); auto with geo. assert (alignes B O O'); auto with geo. halignes H9 x. absurd (B = O); auto. assert (vec O' B = mult_PP x (vec O B)). VReplace (vec O' B) (mult_PP (-1) (vec B O')). rewrite H10; Ringvec. assert (alignes C O O'); auto with geo. halignes H12 k. absurd (C = O); auto. assert (vec O' C = mult_PP k (vec O C)). VReplace (vec O' C) (mult_PP (-1) (vec C O')). rewrite H13; Ringvec. 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 H18; intros; auto. absurd (distance O' A' = 0); auto. elim (Rlt_le_dec x 0); intros. assert (x <= 0); auto with real. assert (B = barycentre (cons (distance O A) O') (cons (distance O' A') O)). apply k_negatif_barycentre with x; auto. elim (Rlt_le_dec k 0); intros. assert (k <= 0); auto with real. assert (C = barycentre (cons (distance O A) O') (cons (distance O' A') O)). apply k_negatif_barycentre with k; auto. rewrite H21; auto. assert (distance O O' = distance O A + distance O' A'). apply k_negatif_distance_centres with (4 := H11); auto. assert (distance O O' = Rabs (distance O A + - distance O' A')). apply k_positif_distance_centres with (4 := H14); auto. auto with real. assert (distance O A = 0 \/ distance O' A' = 0). apply aux_Rpos; auto. rewrite <- H23; auto. elim H24; intros. absurd (distance O A = 0); auto. absurd (distance O' A' = 0); auto. assert (distance O O' = Rabs (distance O A + - distance O' A')). apply k_positif_distance_centres with (4 := H11); auto. auto with real. elim (classic (distance O A = distance O' A')); intros. assert (O = O'). assert (distance O O' = 0); auto with geo. rewrite H20; rewrite H21. RReplace (distance O' A' + - distance O' A') 0. rewrite Rabs_right; auto with real. absurd (cercle_rayon O A A'); auto. icercle. rewrite H21; rewrite H22; auto. 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)))). assert (mult_PP (distance O A) (vec O' B) = mult_PP (distance O' A') (vec O B)). apply point_contact_k_positif with x; auto. auto with real. rewrite H22; Ringvec. assert (distance O A + - distance O' A' <> 0); auto with real. elim (Rlt_le_dec k 0); intros. assert (k <= 0); auto with real. assert (distance O O' = distance O A + distance O' A'). apply k_negatif_distance_centres with (4 := H14); auto. assert (distance O A = 0 \/ distance O' A' = 0). apply aux_Rpos; auto. rewrite <- H25; auto. elim H26; intros. absurd (distance O A = 0); auto. absurd (distance O' A' = 0); auto. assert (mult_PP (distance O A + - distance O' A') (vec O C) = 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 C)) (mult_PP (-1) (mult_PP (distance O A) (vec O' C)))). assert (mult_PP (distance O A) (vec O' C) = mult_PP (distance O' A') (vec O C)). apply point_contact_k_positif with k; auto. auto with real. rewrite H24; Ringvec. apply egalite_vecteur_point with O. assert (vec O B = mult_PP (/ (distance O A + - distance O' A')) (mult_PP (distance O A) (vec O O'))). rewrite <- H22. VReplace (mult_PP (/ (distance O A + - 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 + - distance O' A')) (vec O B)). replace ((distance O A + - distance O' A') * / (distance O A + - distance O' A')) with 1; auto with real. Ringvec. rewrite H25. rewrite <- H24. VReplace (mult_PP (/ (distance O A + - distance O' A')) (mult_PP (distance O A + - distance O' A') (vec O C))) (mult_PP ((distance O A + - distance O' A') * / (distance O A + - distance O' A')) (vec O C)). replace ((distance O A + - distance O' A') * / (distance O A + - distance O' A')) with 1; auto with real. Ringvec. Qed.