proposition: Lemma egalite_forme_polaire : forall z z' : C, z <> zeroC -> z' <> zeroC -> module z = module z' -> argument z = argument z' -> z = z'.
proof: Proof. intros. elim existence_forme_polaire with (z := z); [ intros r H3; elim H3; intros a H4; elim H4; intros H5 H6; try clear H4 H3 existence_forme_polaire; try exact H6 | auto ]. elim existence_forme_polaire with (z := z'); [ intros r0 H7; elim H7; intros a0 H8; elim H8; intros H9 H10; try clear H8 H7 existence_forme_polaire; try exact H10 | auto ]. rewrite (forme_polaire_def (z:=z) (r:=r) (a:=a)); auto. rewrite (forme_polaire_def (z:=z') (r:=r) (a:=a)); auto. rewrite <- H5; auto. rewrite <- H6; auto. Qed.