proposition: Lemma existence_inverse : forall z : C, z <> zeroC -> exists z' : C, Cmult z z' = oneC.
proof: Proof. intros. elim existence_forme_polaire with (z := z); [ intros r H1; elim H1; intros a H2; elim H2; intros H3 H4; try clear H2 H1; try exact H3 | auto with geo ]. cut (r <> 0); intros. cut (/ r <> 0); intros; auto with real. cut (cons_pol (/ r) (- a) <> zeroC); intros. exists (cons_pol (/ r) (- a)). apply egalite_forme_polaire; auto with geo. rewrite Cmult_module; rewrite module_oneC; rewrite complexe_polaire_module; rewrite H3; field; trivial. rewrite Cmult_argument; auto with geo. rewrite complexe_polaire_argument; auto with geo. rewrite H4; rewrite argument_oneC. rewrite <- add_mes_compatible. replace (a + - a) with 0; [ auto | ring ]. auto with real geo. rewrite <- H3; auto with geo. Qed.