fact: Definition SFfrexp f := match f with | S754_finite sx mx ex => if (Z.to_pos prec <=? digits2_pos mx)%positive then (S754_finite sx mx (-prec), (ex+prec)%Z) else let d := (prec - Z.pos (digits2_pos mx))%Z in (S754_finite sx (shift_pos (Z.to_pos d) mx) (-prec), (ex+prec-d)%Z) | _ => (f, (-2*emax-prec)%Z) end.
imports: ZArith FloatClass