proposition: Lemma exists_polar_form : forall z : C, { r : R & { theta : R | z = r * cos (theta) +i r * sin (theta) } }.
proof: Proof. intros [a b] ; destruct (total_order_T a R0) as [[a_neg | a_eq] | a_pos]. assert (Hrew : (sqrt (1 + (b / a) ^ 2) = sqrt (a * a + b * b) / sqrt ((- a) * - a))%R). simpl ; repeat rewrite Rmult_1_r ; rewrite <- sqrt_div. f_equal ; field ; apply Rlt_not_eq ; assumption. left ; apply Rplus_lt_le_0_compat ; [apply sqr_pos_lt, Rlt_not_eq ; assumption | apply sqr_pos]. apply sqr_pos_lt, Rgt_not_eq ; lra. exists (- Cnorm (a +i b))%R ; exists (Ratan.atan (Cim (a +i b) / Cre (a +i b))) ; CusingR_simpl. rewrite Ratan.cos_atan ; unfold Cnorm, Cnorm_sqr ; rewrite Hrew ; simpl ; rewrite sqrt_square. field ; split ; [apply Rlt_not_eq | apply sqrt_no_R0]. assumption. apply Rplus_lt_le_0_compat ; [apply sqr_pos_lt, Rlt_not_eq ; assumption | apply sqr_pos]. lra. rewrite Ratan.sin_atan ; unfold Cnorm, Cnorm_sqr ; rewrite Hrew ; simpl ; rewrite sqrt_square. field ; split ; [apply Rlt_not_eq | apply sqrt_no_R0]. assumption. apply Rplus_lt_le_0_compat ; [apply sqr_pos_lt, Rlt_not_eq ; assumption | apply sqr_pos]. lra. exists b ; exists (PI / 2) ; rewrite cos_PI2, sin_PI2, a_eq ; CusingR. assert (Hrew : (sqrt (1 + (b / a) ^ 2) = sqrt (a * a + b * b) / sqrt (a * a))%R). simpl ; repeat rewrite Rmult_1_r ; rewrite <- sqrt_div. f_equal ; field ; apply Rgt_not_eq ; assumption. left ; apply Rplus_lt_le_0_compat ; [apply sqr_pos_lt, Rgt_not_eq ; assumption | apply sqr_pos]. apply sqr_pos_lt, Rgt_not_eq ; lra. exists (Cnorm (a +i b))%R ; exists (Ratan.atan (Cim (a +i b) / Cre (a +i b))) ; CusingR_simpl. rewrite Ratan.cos_atan ; unfold Cnorm, Cnorm_sqr ; rewrite Hrew ; simpl ; rewrite sqrt_square. field ; split ; [apply Rgt_not_eq | apply sqrt_no_R0]. assumption. apply Rplus_lt_le_0_compat ; [apply sqr_pos_lt, Rgt_not_eq ; assumption | apply sqr_pos]. lra. rewrite Ratan.sin_atan ; unfold Cnorm, Cnorm_sqr ; rewrite Hrew ; simpl ; rewrite sqrt_square. field ; split ; [apply Rgt_not_eq | apply sqrt_no_R0]. assumption. apply Rplus_lt_le_0_compat ; [apply sqr_pos_lt, Rgt_not_eq ; assumption | apply sqr_pos]. lra. Qed.
imports: Rbase AltSeries Rseries_def Rtrigo_facts Ratan Cpow_plus Complex Lra MyRIneq