proposition: Theorem is_nan_Bpred : forall x, is_nan (Bpred x) = is_nan x.
proof: Proof. intros x. unfold Bpred. rewrite is_nan_Bopp, is_nan_Bsucc. apply is_nan_Bopp. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative