proposition: Theorem Rpower_sqrt : forall x:R, 0 < x -> Rpower x (/ 2) = sqrt x.
proof: Proof. intros x H. apply ln_inv. - unfold Rpower; apply exp_pos. - apply sqrt_lt_R0; apply H. - apply Rmult_eq_reg_l with (INR 2). + apply exp_inv. fold Rpower. cut (Rpower (Rpower x (/ INR 2)) (INR 2) = Rpower (sqrt x) (INR 2)). * unfold Rpower; auto. * rewrite Rpower_mult. rewrite Rinv_l. -- change 1 with (INR 1). repeat rewrite Rpower_pow; simpl. ++ pattern x at 1; rewrite <- (sqrt_sqrt x (Rlt_le _ _ H)). ring. ++ apply sqrt_lt_R0; apply H. ++ apply H. -- apply not_O_INR; discriminate. + apply not_O_INR; discriminate. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra