proposition: Theorem Btrunc_correct : forall x, IZR (Btrunc x) = round radix2 (FIX_exp 0) Ztrunc (B2R x).
proof: Proof. intros x. rewrite <-B2R_B2BSN. now apply Btrunc_correct. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN