proposition: Theorem inversion_negatif_complexe : forall (k : R) (z z' : C) (M M' : PO), O <> M :>PO -> k < 0 -> z = affixe_vec (vec O M) :>C -> z' = affixe_vec (vec O M') :>C -> M' = inversion O k M :>PO -> z' = Cmult (Rinj k) (Cinv (Conj z)).
proof: Proof. intros. assert (k <> 0); auto with real. assert (z <> zeroC). apply points_distincts_non_zeroC with (1 := H); auto with geo. assert (Conj z <> zeroC); auto with geo. let N := fresh "N" in symetrique O M N. assert (M' = inversion O (- k) N). apply inversion_oppose_puissance with (3 := H3); auto. assert (- k > 0); auto with real. assert (O <> N). assert (O = homothetie (-1) O O); auto with geo. unfold symetrie in H5. apply (image_homothetie_distincts (k:=-1) (I:=O) (A:=O) (A':=O) (B:=M) (B':=N)); auto with real. rewrite (inversion_positif_complexe (k:=- k) (z:=Copp z) (z':=z') (M:=N) (M':=M')) ; auto. rewrite Rinj_opp. rewrite Conj_Copp. rewrite Cinv_Copp; auto. ring. symmetry in |- *. rewrite (produit_vecteur_image (k:=-1) (z:=z) (z':=affixe_vec (vec O N)) (A:=O) (B:=M) (A':=O) (B':=N)); auto. replace (Rinj (-1)) with (Copp oneC). ring. unfold oneC, Rinj in |- *. rewrite Copp_algebrique; auto. RReplace (-0) 0; auto. VReplace (mult_PP (-1) (vec O M)) (vec M O). rewrite (milieu_vecteur H8); auto. Qed.