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. split. - easy. - unfold pow2_UP. unfold Xscale. destruct sensible_format eqn:H1. + rewrite scale2_correct by easy. unfold toX, toF, FtoX. generalize (mantissa_sign_correct (mantissa_pos mantissa_one)). rewrite mantissa_pos_correct by apply mantissa_one_correct. rewrite (proj1 mantissa_one_correct). destruct mantissa_sign. * easy. * destruct s0; [easy |]. unfold FtoR. rewrite exponent_zero_correct. intros [<- _]. apply le_upper_refl. + easy. Qed.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig