proposition: Lemma cercle_inversion_homothetie : forall (A A' B B' I A1 B1 : PO) (k : R), k <> 0 -> triangle A B I -> B <> B' -> I <> A' -> triangle A A' B -> sont_cocycliques A A' B B' -> alignes A A' I -> alignes B B' I -> A1 = inversion I k A -> B1 = inversion I k B -> A1 = homothetie (k * / scalaire (vec I A) (vec I A')) I A' /\ B1 = homothetie (k * / scalaire (vec I A) (vec I A')) I B'.
proof: Proof. intros. assert (scalaire (vec I A) (vec I A') = scalaire (vec I B) (vec I B')). apply puissance_cercle; auto. deroule_triangle A B I. deroule_triangle A A' B. assert (alignes I A A'); auto with geo. assert (alignes I B B'); auto with geo. halignes H18 x. absurd (I = A); auto. halignes H19 y. absurd (I = B); auto. assert (distance I A <> 0); auto with geo real. assert (distance I A * distance I A <> 0). unfold Rsqr in |- *; auto with real. assert (scalaire (vec I A) (vec I A') <> 0). red in |- *; intros; apply H2. apply (produit_zero_conf H20). apply Rmult_eq_reg_l with (scalaire (vec I A) (vec I A)). RReplace (scalaire (vec I A) (vec I A) * 0) 0. rewrite <- H24. rewrite H20; Simplscal. rewrite carre_scalaire_distance; auto. assert (x <> 0). contrapose H24. rewrite H20; rewrite H25; Simplscal. split; [ try assumption | idtac ]. apply vecteur_homothetie. rewrite (inversion_pole_vecteur (k:=k) (O:=I) (M:=A) (M':=A1)); auto. rewrite H20; 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)). replace (/ (distance I A * distance I A) * k) with (k * (/ (distance I A * distance I A) * (/x * x))); auto. field; auto. field; auto. apply vecteur_homothetie. rewrite (inversion_pole_vecteur (k:=k) (O:=I) (M:=B) (M':=B1)); auto. rewrite H9. rewrite H21; Simplscal. rewrite carre_scalaire_distance. unfold Rsqr in |- *. assert (distance I B <> 0); auto with geo real. assert (distance I B * distance I B <> 0). unfold Rsqr in |- *; auto with real. assert (scalaire (vec I B) (vec I B') <> 0). rewrite <- H9; auto. assert (y <> 0). contrapose H26. rewrite H21; rewrite H29; Simplscal. RReplace (/ (y * (distance I B * distance I B))) (/ y * / (distance I B * distance I B)). VReplace (mult_PP (k * (/ y * / (distance I B * distance I B))) (mult_PP y (vec I B))) (mult_PP (k * (/ (distance I B * distance I B) * (/ y * y))) (vec I B)). replace (/ (distance I B * distance I B) * k) with (k * (/ (distance I B * distance I B) * (/ y * y))); auto. field;auto. field;auto. Qed.