proposition: Lemma cercle_tangente_inversion_homothetie : forall (A A' B M I M' O : PO) (k : R), k <> 0 -> A <> B -> I <> A -> I <> M -> cercle_diametre A B M -> O = milieu A B -> orthogonal (vec M O) (vec M I) -> alignes A B I -> A' = inversion I k A -> M' = inversion I k M -> A' = homothetie (k * / scalaire (vec I A) (vec I B)) I B /\ M' = homothetie (k * / scalaire (vec I A) (vec I B)) I M.
proof: Proof. intros. assert (scalaire (vec I A) (vec I B) = Rsqr (distance I O) + - Rsqr (distance O A)). apply scalaire_diametre with B; auto with geo. elim (Pythagore M I O); intros. assert (scalaire (vec I A) (vec I B) = Rsqr (distance I M)). rewrite H9. rewrite H10; auto with geo. rewrite (distance_sym M O). replace (Rsqr (distance O M)) with (Rsqr (distance O A)). rewrite distance_sym; ring. hcercle H3. elim H12; [ intros O0 H13; elim H13; [ intros H14 H15; elim H14; [ intros H16 H17; try clear H14 H13 H12; try exact H17 ] ] ]. assert (O0 = O). rewrite H4; auto. rewrite <- H12; rewrite H17; auto. assert (alignes I A B); auto with geo. halignes H13 x. assert (distance I A <> 0); auto with geo real. assert (distance I A * distance I A <> 0). unfold Rsqr in |- *; auto with real. assert (distance I M <> 0); auto with geo real. assert (distance I M * distance I M <> 0). unfold Rsqr in |- *; auto with real. assert (scalaire (vec I A) (vec I B) <> 0). rewrite H12. unfold Rsqr in |- *; auto. assert (x <> 0). contrapose H18. rewrite H14; rewrite H20; Simplscal. split; [ try assumption | idtac ]. apply vecteur_homothetie. rewrite (inversion_pole_vecteur (k:=k) (O:=I) (M:=A) (M':=A')); auto. rewrite H14; Simplscal. rewrite carre_scalaire_distance. unfold Rsqr in |- *. RReplace (/ (x * (distance I A * distance I A))) (/ x * / (distance I A * distance I A)). VReplace (mult_PP (k * (/ x * / (distance I A * distance I A))) (mult_PP x (vec I A))) (mult_PP (k * (/ (distance I A * distance I A) * (/ x * x))) (vec I A)). RReplace (/ x * x) 1. RReplace (/ (distance I A * distance I A) * k) (k * (/ (distance I A * distance I A) * 1)); auto. rewrite <- Rinv_mult; auto. RReplace (distance I A * distance I A * x) (x * (distance I A * distance I A)); auto. apply vecteur_homothetie. rewrite (inversion_pole_vecteur (k:=k) (O:=I) (M:=M) (M':=M')); auto. rewrite H12. unfold Rsqr in |- *. Ringvec. Qed.