proposition: Theorem shr_fexp_truncate : forall m e l, (0 <= m)%Z -> shr_fexp m e l = let '(m', e', l') := truncate radix2 fexp (m, e, l) in (shr_record_of_loc m' l', e').
proof: Proof. intros m e l. now apply shr_fexp_truncate. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN