proposition: Theorem inversion_complexe : forall (k : R) (j z z' : C) (J M M' : PO), J <> M -> k <> 0 -> z = affixe M -> z' = affixe M' -> j = affixe J -> M' = inversion J k M -> Cplus z' (Copp j) = Cmult (Rinj k) (Cinv (Conj (Cplus z (Copp j)))).
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. assert (vec J M' = mult_PP (/ Rsqr (distance J M) * k) (vec J M)). apply homothetie_vecteur. apply inversion_homothetie; auto. generalize H8. replace (Rsqr (distance J M)) with (Rsqr (distance O N)). rewrite <- H6; rewrite <- H5; intros. assert (N' = inversion O k N). apply homothetie_inversion; auto. apply vecteur_homothetie; auto. rewrite (affixe_vec_AB H3 H2). rewrite (affixe_vec_AB H3 H1). rewrite <- H6; rewrite <- H5. elim existence_affixe_vecteur_point with (M := N); intros z1; intros. elim existence_affixe_vecteur_point with (M := N'); intros z2; intros. rewrite <- H12; rewrite <- H11. apply inversion_pole_origine_complexe with (5 := H10); auto. unfold Rsqr in |- *. repeat rewrite <- carre_scalaire_distance. rewrite H5; auto. Qed.