proposition: Lemma pow2_UP_correct : forall p s, (valid_ub (pow2_UP p s) = true /\ le_upper (Xscale radix2 (Xreal 1) (StoZ s)) (toX (pow2_UP p s))).
proof: Proof. intros p s. split; [easy |]. simpl. rewrite Rmult_1_l. unfold pow2_UP, Fpow2, toX. generalize (radix_prop radix). destruct (radix_val radix) as [|[r|r|]|r] eqn:H ; try easy ; intros _. - unfold Fscale2; rewrite H. destruct s as [|s|s]; [apply Rle_refl| |easy]. rewrite iter_pos_nat. simpl. apply IZR_le. rewrite Zpower_pos_nat. apply Zeq_le. induction (Pos.to_nat s). easy. rewrite iter_nat_S. now rewrite Zpower_nat_S, IHn. - rewrite Fscale2_correct by now rewrite H. simpl. unfold StoZ. rewrite Rmult_1_l. apply Rle_refl. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Zaux Raux) Xreal Basic Generic Generic_proof Sig