proposition: Lemma exists_principal_polar_form : forall z : C, { r : R & { theta : R | 0 <= r /\ 0 < theta <= 2 * PI /\ r * cos (theta) +i r * sin (theta) = z } }%R.
proof: Proof. intro z ; destruct (exists_polar_form z) as [r [theta Hr]] ; destruct (Rlt_le_dec r 0) as [r_neg | r_pos]. exists (- r) ; destruct (x_modulo_2PI (theta + PI)) as [k Hk] ; exists (theta + PI + 2 * IZR k * PI) ; split ; [| split]. lra. replace (theta + PI + 2 * IZR k * PI) with (IZR k * (2 * PI) + (theta + PI)) by ring ; assumption. subst ; CusingR. rewrite <- cos2PI_period, neg_cos ; ring. rewrite <- sin2PI_period, neg_sin ; ring. exists r ; destruct (x_modulo_2PI theta) as [k Hk] ; exists (theta + 2 * IZR k * PI) ; split ; [| split]. assumption. replace (theta + 2 * IZR k * PI) with (IZR k * (2 * PI) + theta) by ring ; assumption. subst ; CusingR ; [rewrite <- cos2PI_period | rewrite <- sin2PI_period] ; ring. Qed.
imports: Rbase AltSeries Rseries_def Rtrigo_facts Ratan Cpow_plus Complex Lra MyRIneq