proposition: Theorem complexe_inversion_pole_origine : 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 -> z' = Cmult (Rinj k) (Cinv (Conj z)) -> M' = inversion O k M :>PO.
proof: Proof. intros. apply homothetie_inversion; auto. apply vecteur_homothetie; auto. apply (produit_reel_affixe_vecteur_OM (k:=/ Rsqr (distance O M) * k) (z:=z) (z':=z') (M:=M) (M':=M')); auto. rewrite H3. rewrite Rinj_Cmult. assert (z <> zeroC). apply points_distincts_non_zeroC with (1 := H); auto with geo. assert (Conj z <> zeroC); auto with geo. rewrite <- (module_def2 (z:=z) (M:=M)); auto with geo. rewrite Rinj_Cinv. rewrite <- produit_Conj_module. rewrite Cinv_Cmult; auto. replace (Cmult (Cmult (Cmult (Cinv z) (Cinv (Conj z))) (Rinj k)) z) with (Cmult (Cmult z (Cinv z)) (Cmult (Cinv (Conj z)) (Rinj k))). 2: ring. rewrite Cinv_def; auto. ring. unfold Rsqr in |- *. assert (module z <> 0); auto with geo. Qed.