proposition: Lemma inversion_pole_origine_analytique : forall (k : R) (M M' : PO), O <> M :>PO -> k <> 0 -> M' = inversion O k M :>PO -> abscisse M' = k * abscisse M / (Rsqr (abscisse M) + Rsqr (ordonnee M)) /\ ordonnee M' = k * ordonnee M / (Rsqr (abscisse M) + Rsqr (ordonnee M)).
proof: Proof. intros. paffixe M z. paffixe M' z'. assert (z <> zeroC). apply points_distincts_non_zeroC with (1 := H); auto with geo. assert (module z <> 0); auto with geo. assert (Rsqr (module z) <> 0). unfold Rsqr in |- *; auto with real. generalize H3 H2. repeat rewrite <- coordonnees_affixe; intros. assert (z' = Cmult (Rinj k) (Cinv (Conj z))). apply inversion_pole_origine_complexe with (5 := H1); auto with geo. apply unicite_parties_relles_imaginaires with z'; auto. rewrite H9. rewrite Conj_Cinv; auto. rewrite <- Rinj_Cinv; auto. ring_simplify. rewrite <- Rinj_Cmult. rewrite (carre_module H8). rewrite H8. rewrite Cmult_Rinj_algebrique. unfold Rdiv in |- *. replace (k * / (Rsqr (abscisse M) + Rsqr (ordonnee M)) * abscisse M) with (k * abscisse M * / (Rsqr (abscisse M) + Rsqr (ordonnee M))) by ring. replace (k * / (Rsqr (abscisse M) + Rsqr (ordonnee M)) * ordonnee M) with(k * ordonnee M * / (Rsqr (abscisse M) + Rsqr (ordonnee M))) by ring. auto. Qed.