proposition: Lemma exist_root_n_pos : forall r n, r >= 0 -> (n > 0)%nat -> {root | root ^ n = r}%R.
proof: Proof. intros r n Hr Hn. pose (f := (fun x => x ^ n - r)%R). assert (Cont_pow : forall x, continuity_pt f x). unfold f. intros x. reg. destruct (total_order_T r 0) as [[order|order]|order]. edestruct Rge_not_lt; eauto. exists 0. rewrite order. rewrite pow_ne_zero. reflexivity. intuition. assert (Hsup0 : r+1 > 0) by lra. assert (Hpos : forall n, (n > 0)%nat -> (r + 1) ^ n - r > 0). intros n1 Hn1. apply ast_fun_pos. assumption. assumption. assert (Hneg : 0 ^ n - r < 0). rewrite pow_ne_zero. lra. intuition. generalize (IVT (fun x => x ^ n - r) 0 (r + 1) Cont_pow Hsup0 Hneg)%R. intros H. destruct H as (x, H). apply Hpos. assumption. exists x. intuition. Qed.
imports: Complex Cpow_plus Cpolar Cexp