proposition: Theorem complexe_inversion : forall (k : R) (j z z' : C) (J M M' : PO), J <> M -> k <> 0 -> z = affixe M -> z' = affixe M' -> j = affixe J -> Cplus z' (Copp j) = Cmult (Rinj k) (Cinv (Conj (Cplus z (Copp j)))) -> M' = inversion J k M.
proof: Proof. intros. elim existence_representant_vecteur with (A := O) (B := J) (C := M); intros N; intros. elim existence_representant_vecteur with (A := O) (B := J) (C := M'); intros N'; intros. assert (O <> N). apply distinct_egalite_vecteur with (2 := H5); auto. apply homothetie_inversion; auto. apply vecteur_homothetie. rewrite <- H6; rewrite <- H5. replace (Rsqr (distance J M)) with (Rsqr (distance O N)). assert (N' = inversion O k N). apply complexe_inversion_pole_origine with (5 := H4); auto. rewrite H5; auto with geo. rewrite H6; auto with geo. apply homothetie_vecteur. apply inversion_homothetie; auto. unfold Rsqr in |- *. repeat rewrite <- carre_scalaire_distance. rewrite H5; auto. Qed.