proposition: Lemma inversion_origine_module : forall (k : R) (z z' : C) (M M' : PO), k <> 0 -> O <> M -> z = affixe_vec (vec O M) -> z' = affixe_vec (vec O M') -> M' = inversion O k M :>PO -> module z' = Rabs k * / module z.
proof: Proof. intros. assert (vec O M' = mult_PP (/ Rsqr (distance O M) * k) (vec O M)). apply inversion_pole_vecteur; auto. assert (module z <> 0). apply module_non_zero. apply points_distincts_non_zeroC with (1 := H0); auto with geo. RReplace (/ module z) (1 * / module z). RReplace 1 (/ module z * module z). RReplace (/ module z * module z * / module z) (/ module z * / module z * module z). replace (/ module z * / module z) with (/ Rsqr (module z)). pattern (module z) at 1 in |- *. rewrite (module_def2 (z:=z) (M:=M)); auto with geo. RReplace (Rabs k * (/ Rsqr (distance O M) * module z)) (/ Rsqr (distance O M) * Rabs k * module z). replace (/ Rsqr (distance O M) * Rabs k) with (Rabs (/ Rsqr (distance O M) * k)). apply (module_affixe_produit_vecteur_OM (k:=/ Rsqr (distance O M) * k) (M:=M) (M':=M') (z:=z) (z':=z')); auto with geo. rewrite Rabs_mult. rewrite <- (module_def2 (z:=z) (M:=M)); auto with geo. unfold Rsqr in |- *. rewrite Rabs_inv; auto with real. rewrite Rabs_right; auto with geo real. unfold Rsqr in |- *. rewrite Rinv_mult; auto with real. Qed.