proposition: Theorem inversion_droite_non_pole : forall (A B M M' I : PO) (k : R), k <> 0 -> triangle A B I -> I <> M -> alignes A B M -> M' = inversion I k M -> exists C : PO, orthogonal (vec A B) (vec I C) /\ cercle_diametre I C M'.
proof: Proof. intros. deroule_triangle A B I. soit_projete A B I K. assert (I <> K). red in |- *; intros; apply H4. rewrite H11; auto. image_inversion I K K' k. exists K'. unfold cercle_diametre in |- *. soit_milieu I K' D. deroule_inversion I M M' k. soit_projete I M K' L. halignes H2 x. halignes H9 y. assert (vec K M = mult_PP (x + - y) (vec A B)). VReplace (vec K M) (add_PP (vec A M) (mult_PP (-1) (vec A K))). rewrite H26; rewrite H25; Ringvec. halignes H13 z. assert (orthogonal (vec I K') (vec A B)). rewrite H28; Simplortho. split; [ auto with geo | idtac ]. exists D; (split; auto). assert (scalaire (vec I M) (vec I K') = scalaire (vec I M) (vec I L)). apply (scalaire_avec_projete (A:=I) (B:=M) (C:=K') (H:=L)); auto with geo. assert (scalaire (vec I K') (vec I M) = scalaire (vec I K') (vec I K)). apply (scalaire_avec_projete (A:=I) (B:=K') (C:=M) (H:=K)); auto with geo. apply ortho_sym. rewrite H27; Simplortho. assert (scalaire (vec I M) (vec I L) = scalaire (vec I M) (vec I M')). rewrite <- H30; rewrite scalaire_sym; rewrite H31; rewrite scalaire_sym; rewrite H14; auto. assert (L = M'). apply egalite_scalaire_alignes with (4 := H32); auto. rewrite <- H33; auto with geo. discrimine L K'. icercle. assert (orthogonal (vec L I) (vec L K')). halignes H23 t. VReplace (vec L I) (mult_PP (-1) (vec I L)). rewrite H35. VReplace (mult_PP (-1) (mult_PP t (vec I M))) (mult_PP (- t) (vec I M)). auto with geo. assert (triangle L I K'). unfold triangle in |- *. apply orthogonal_non_alignes; auto. rewrite H33; auto. elim existence_cercle_circonscrit with (A := I) (B := K') (C := L); [ intros O H37 | auto with geo ]. cut (O = D); intros. rewrite <- H38; auto. apply (centre_circonscrit_rectangle_milieu (A:=I) (B:=K') (C:=L) (C':=D) (O:=O)); auto with geo. Qed.