proposition: Theorem inversion_cercle_diametre_pole : forall (A M A' M' I : PO) (k : R), k <> 0 -> triangle I A M -> A' = inversion I k A -> M' = inversion I k M -> cercle_diametre I A M -> droite_perpendiculaire I A A' M'.
proof: Proof. unfold droite_perpendiculaire in |- *; intros A M A' M' I k H H0 H2 H3 H1. generalize H1; unfold cercle_diametre in |- *; intros. elim H4; [ intros O H5; elim H5; [ intros H6 H7; try clear H5 H4; try exact H7 ] ]. assert (orthogonal (vec M I) (vec M A)). apply triangle_diametre with O; auto with geo. hcercle H6. rewrite <- H8; auto. deroule_triangle I A M. deroule_inversion I A A' k. deroule_inversion I M M' k. elim existence_projete_orthogonal with (A := I) (B := A) (C := M'); [ intros H' H17; try clear existence_projete_orthogonal; try exact H16 | auto ]. elim def_projete_orthogonal2 with (A := I) (B := A) (C := M') (H := H'); [ intros; try clear def_projete_orthogonal2; try exact H17 | auto | auto ]. halignes H14 x. halignes H18 y. assert (scalaire (vec I M') (vec I A) = scalaire (vec I M') (vec I M)). apply (scalaire_avec_projete (A:=I) (B:=M') (C:=A) (H:=M)); auto with geo. rewrite H20; Simplortho. assert (scalaire (vec I A) (vec I M') = scalaire (vec I A) (vec I H')). apply (scalaire_avec_projete (A:=I) (B:=A) (C:=M') (H:=H')); auto with geo. assert (scalaire (vec I A) (vec I A') = scalaire (vec I A) (vec I H')). rewrite H12; rewrite <- H15. rewrite scalaire_sym; rewrite <- H22. rewrite scalaire_sym; rewrite H23; auto. assert (A' = H'). apply egalite_scalaire_alignes with (4 := H24); auto with geo. rewrite H25; auto with geo. Qed.