proposition: Lemma valid_ub_next_up x : valid_ub (next_up x) = true.
proof: Proof. rewrite valid_ub_correct. unfold classify. rewrite classify_spec. rewrite <-B2SF_Prim2B, next_up_equiv. case Prim2B as [s|s| |s m e B]; [now simpl|now case s|now simpl| ]. generalize (Bsucc_correct _ _ _ _ (B754_finite s m e B) (refl_equal _)). case Rlt_bool; [ |now intros ->]. intros [_ [H _]]; revert H. case Bsucc as [s'|s'| |s' m' e' B']; [now case s'|now simpl..| ]. intros _; simpl. now set (d := match digits2_pos m' with 53%positive => _ | _ => _ end); case s', d. Qed.
imports: Coq(ZArith Reals) Int63Compat Coq(Floats Psatz) Flocq(Zaux Raux BinarySingleNaN PrimFloat Sterbenz Mult_error) Missing.Stdlib Missing.Flocq Xreal Basic Sig