proposition: Lemma Fpower_pos_dn_correct : forall prec x n, le_lower' (Xreal 0) (F.toX x) -> F.valid_lb (Fpower_pos_DN prec x n) = true /\ le_lower' (F.toX (Fpower_pos_DN prec x n)) (Xpower_int (F.toX x) (Zpos n)).
proof: Proof. intros prec x n. xreal_tac2; [now simpl|]. simpl. intro Hx. set (p := Fpower_pos_DN prec x n). cut (F.valid_lb p = true /\ le_lower' (F.toX p) (Xreal (r ^ Pos.to_nat n))). { now simpl. } unfold p; clear p. revert x r X Hx. unfold le_lower'. induction n ; intros x rx Hrx Hx ; simpl; last first. { split. { now rewrite F'.valid_lb_real; [|rewrite F.real_correct, Hrx]. } now rewrite Hrx, Rmult_1_r; right. } { rewrite F.cmp_correct, F.zero_correct, F'.classify_zero. elim (F.mul_DN_correct prec x x); [|now left; unfold F.is_non_neg_real; rewrite Hrx]. intros Vmdn Hmdn. generalize Vmdn; rewrite F.valid_lb_correct. case F.classify; [..|easy]; intros _. 2: now rewrite F'.valid_lb_nan, F'.nan_correct. 2: { rewrite F'.valid_lb_zero, F.zero_correct; split; [easy|]. rewrite Pos2Nat.inj_xO, pow_sqr. apply pow_le, Rle_0_sqr. } unfold Xcmp. xreal_tac2; [now rewrite F'.valid_lb_nan, F'.nan_correct|]. case Rcompare_spec; intro Hr0; [rewrite F'.valid_lb_zero, F.zero_correct; split; [easy|] ; rewrite Pos2Nat.inj_xO, pow_sqr ; apply pow_le, Rle_0_sqr..|]. rewrite Pos2Nat.inj_xO, pow_sqr. generalize (IHn _ _ X (Rlt_le _ _ Hr0)). intros [Vp Hp]; split; [exact Vp|]. revert Hp; xreal_tac2; [easy|]; intro Hp. apply (Rle_trans _ _ _ Hp). apply pow_incr. split; [now left|]. apply Ropp_le_cancel. change (_ <= _)%R with (le_lower (Xreal r) (Xmul (Xreal rx) (Xreal rx))). now rewrite <-Hrx. } rewrite F.cmp_correct, F.zero_correct, F'.classify_zero. elim (F.mul_DN_correct prec x x); [|now left; unfold F.is_non_neg_real; rewrite Hrx]. intros Vmdn Hmdn. generalize Vmdn; rewrite F.valid_lb_correct. case F.classify; [..|easy]; intros _. 2: now rewrite F'.valid_lb_nan, F'.nan_correct. 2: { rewrite F'.valid_lb_zero, F.zero_correct; split; [easy|]. apply (Rmult_le_pos _ _ Hx). rewrite Pmult_nat_mult, Nat.mul_comm, pow_sqr. apply pow_le, Rle_0_sqr. } unfold Xcmp. xreal_tac2; [now rewrite F'.valid_lb_nan, F'.nan_correct|]. case Rcompare_spec; intro Hr0; [rewrite F'.valid_lb_zero, F.zero_correct; split; [easy|]; apply (Rmult_le_pos _ _ Hx); rewrite Pmult_nat_mult, Nat.mul_comm, pow_sqr; apply pow_le, Rle_0_sqr..|]. elim (IHn _ _ X (Rlt_le _ _ Hr0)). intros Vp Hp. elim (F'.mul_DN_correct prec x (Fpower_pos_DN prec (F.mul_DN prec x x) n)). 2:{ unfold F.is_non_neg_real, F.is_non_pos_real, F.is_non_neg, F.is_non_pos. rewrite Hrx, F'.valid_ub_real, Vp; [|now rewrite F.real_correct, Hrx]. xreal_tac2; [now right; right; left|]. now case (Rle_or_lt 0 r0); intro H0r0; [left|right; right; left; repeat split; lra]. } intros Vxp Hxp; split; [easy|]. revert Hxp; rewrite Hrx. do 2 (xreal_tac2; [easy|]). unfold le_lower; intro H; apply Ropp_le_cancel in H. apply (Rle_trans _ _ _ H); clear H. apply (Rmult_le_compat_l _ _ _ Hx). apply (Rle_trans _ _ _ Hp). rewrite Pmult_nat_mult, Nat.mul_comm, pow_sqr. apply pow_incr; split; [now apply Rlt_le|]. rewrite Hrx in Hmdn. now apply Ropp_le_cancel in Hmdn. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval