proposition: Lemma Cinv_algebrique : forall (z : C) (x y : R), z <> zeroC -> z = cons_cart x y -> Cinv z = cons_cart (x / (Rsqr x + Rsqr y)) (- y / (Rsqr x + Rsqr y)).
proof: Proof. intros. assert (module z <> 0); auto with geo. assert (Rsqr (module z) <> 0). unfold Rsqr in |- *; auto with real. rewrite Cinv_Conj; auto. rewrite (Conj_def H0); auto. rewrite <- Rinj_Cinv; auto. rewrite Cmult_Rinj_algebrique. rewrite (carre_module H0); auto. unfold Rdiv in |- *. RReplace (/ (Rsqr x + Rsqr y) * x) (x * / (Rsqr x + Rsqr y)). RReplace (/ (Rsqr x + Rsqr y) * - y) (- y * / (Rsqr x + Rsqr y)); auto. Qed.