proposition: Theorem next_down_equiv : forall x, Prim2B (next_down x) = Bpred (Prim2B x).
proof: Proof. intro x. apply B2Prim_inj. rewrite B2Prim_Prim2B. apply Prim2SF_inj. rewrite Prim2SF_B2Prim. rewrite next_down_spec. rewrite <-B2SF_Prim2B. unfold Bpred. rewrite <-(Prim2B_B2Prim (Bopp (Prim2B x))). rewrite <-next_up_equiv, <-opp_equiv, !B2SF_Prim2B, opp_spec, next_up_spec. unfold SF64pred, SFpred, SF64succ. do 2 f_equal. now rewrite <-opp_equiv, B2Prim_Prim2B, opp_spec. Qed.
imports: Int63Compat Coq(ZArith Reals Floats SpecFloat) Zaux BinarySingleNaN