proposition: Lemma Bsucc_correct : forall x, is_finite x = true -> if Rlt_bool (succ radix2 fexp (B2R x)) (bpow radix2 emax) then B2R (Bsucc x) = succ radix2 fexp (B2R x) /\ is_finite (Bsucc x) = true /\ (Bsign (Bsucc x) = Bsign x && is_finite_strict x)%bool else B2FF (Bsucc x) = F754_infinity false.
proof: Proof. intros x Fx. rewrite <- is_finite_B2BSN in Fx. generalize (Bsucc_correct prec emax _ _ _ Fx). replace (BinarySingleNaN.Bsucc (B2BSN x)) with (B2BSN (Bsucc x)) by apply B2BSN_lift. rewrite 2!B2R_B2BSN. destruct Rlt_bool. - rewrite (Bsign_B2BSN x) by now destruct x. rewrite is_finite_strict_B2BSN. now destruct Bsucc. - now destruct Bsucc as [|[|]| |]. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN