proposition: Theorem inversion_cercle_non_pole : forall (A B M A' B' M' I : PO) (k : R), k <> 0 -> A <> B -> ~ cercle_diametre A B I -> alignes A B I -> A' = inversion I k A -> B' = inversion I k B -> M' = inversion I k M -> cercle_diametre A B M -> cercle_diametre A' B' M'.
proof: Proof. intros A B M A' B' M' I k H H50 H0 H1 H2 H3 H4 H5; try assumption. assert (I <> A). red in |- *; intros; apply H0. rewrite H6; auto with geo. assert (I <> B). red in |- *; intros; apply H0. rewrite H7; auto with geo. assert (I <> M). red in |- *; intros; apply H0. rewrite H8; auto with geo. elim (classic (alignes A B M)); intros. assert (M = A \/ M = B). apply alignes_diametre; auto. elim H10; [ intros H11; try clear H10 | intros H11; try clear H10; try exact H11 ]. rewrite H4; rewrite H11; rewrite <- H2; auto with geo. rewrite H4; rewrite H11; rewrite <- H3; auto with geo. generalize H5. unfold cercle_diametre, circonscrit, isocele in H5; intros. elim H5; [ intros O H11; elim H11; [ intros H12 H13; elim H12; [ intros H14 H15; try clear H12 H11 H5; try exact H15 ] ] ]. soit_projete M I O K. assert (scalaire (vec I A) (vec I B) <> 0); [ idtac | auto with real ]. assert (alignes I A B); auto with geo. halignes H16 x. rewrite H17. Simplscal. apply integre_not; auto with geo. apply (distinct_col_nonzero (A:=I) (B:=B) (C:=I) (D:=A)); auto. discrimine M K. 2: assert (distance O K < distance O M). rewrite <- H17 in H12. elim cercle_tangente_inversion_homothetie with (A := A) (A' := A') (B := B) (M := M) (I := I) (M' := M') (O := O) (k := k); [ intros | auto | auto | auto | auto | auto with geo | auto | auto with geo | auto | auto | auto ]. elim cercle_tangente_inversion_homothetie with (A := B) (A' := B') (B := A) (M := M) (I := I) (M' := M') (O := O) (k := k); (intros; auto with geo). apply (homothetie_cercle_diametre (k:=k * / scalaire (vec I A) (vec I B)) (I:=I) (A:=B) (A':=A') (B:=A) (B':=B') (M:=M) (M':=M')); auto with geo. apply integre_not; auto with real. rewrite scalaire_sym; auto. apply projete_distance_Rlt with I; auto. apply def_projete_orthogonal; auto with geo. elim intersection2_cercle_droite with (A := M) (B := I) (O := O) (H := K); [ intros C H19; elim H19; [ intros H21 H20; elim H20; [ intros; try clear H20 H19 ] ] | auto | auto | auto | auto ]. assert (triangle A B M). unfold triangle in |- *; auto. halignes H1 y. assert (triangle A M I); unfold triangle in |- *. red in |- *; intros; apply H9. assert (alignes A I M); auto with geo. halignes H25 x. absurd (A = I); auto. apply colineaire_alignes with (x * y). rewrite H26; rewrite H20; Ringvec. assert (sont_cocycliques A B M C). hcercle H23. hcercle H10. elim H26; [ intros O0 H28; elim H28; [ intros H29 H30; elim H29; [ intros H31 H32; try clear H29 H28 H27; try exact H32 ] ] ]. exists O; split; try split; auto with geo. assert (O0 = O). rewrite H30; auto. rewrite H15; rewrite H25; auto. assert (alignes M C I). apply alignes_ordre_permute; auto. elim cercle_inversion_homothetie with (A := A) (A' := B) (B := M) (B' := C) (I := I) (A1 := A') (B1 := M') (k := k); [ intros | auto | auto | auto | auto | auto | auto | auto | auto | auto | auto ]. elim cercle_inversion_homothetie with (A := B) (A' := A) (B := M) (B' := C) (I := I) (A1 := B') (B1 := M') (k := k); [ intros | auto | auto | auto | auto | auto | auto | auto | auto | auto | auto ]. apply (homothetie_cercle_diametre (k:=k * / scalaire (vec I B) (vec I A)) (I:=I) (A:=B) (A':=A') (B:=A) (B':=B') (M:=C) (M':=M')); auto. rewrite scalaire_sym; apply integre_not; auto with real. rewrite scalaire_sym; auto. hcercle H23. hcercle H10. elim H32; [ intros O0 H33; elim H33; [ intros H34 H35; elim H34; [ intros H36 H37; try clear H34 H33 H32; try exact H37 ] ] ]. exists O; split; try split; auto with geo. assert (O0 = O). rewrite H35; auto. rewrite <- H14; rewrite <- H31; rewrite <- H32; auto. unfold triangle in |- *. red in |- *; intros; apply H9. assert (alignes I B M); auto with geo. halignes H30 x. apply colineaire_alignes with (x * (1 + - y) + y). VReplace (vec A M) (add_PP (vec A I) (vec I M)). rewrite H31. VReplace (vec I B) (add_PP (vec A B) (mult_PP (-1) (vec A I))). rewrite H20; Ringvec. auto with geo. auto with geo. auto with geo. auto with geo. elim circonscrit_triangle_non_point with (O := O) (A := A) (B := B) (C := M); [ intros H27 H28; elim H28; [ intros H29 H30; try clear H28; try exact H30 ] | auto | auto ]. hcercle H10. Qed.