proposition: Lemma Bpred_correct : forall x, is_finite x = true -> if Rlt_bool (- bpow radix2 emax) (pred radix2 fexp (B2R x)) then B2R (Bpred x) = pred radix2 fexp (B2R x) /\ is_finite (Bpred x) = true /\ (Bsign (Bpred x) = Bsign x || negb (is_finite_strict x))%bool else B2FF (Bpred x) = F754_infinity true.
proof: Proof. intros x Fx. rewrite <- is_finite_B2BSN in Fx. generalize (Bpred_correct prec emax _ _ _ Fx). replace (BinarySingleNaN.Bpred (B2BSN x)) with (B2BSN (Bpred 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 Bpred. - now destruct Bpred as [|[|]| |]. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN