fact: Definition SFsucc x := match x with | S754_zero _ => SFldexp SFone emin | S754_infinity false => x | S754_infinity true => SFopp SFmax_float | S754_nan => x | S754_finite false _ _ => SFadd x (SFulp x) | S754_finite true _ _ => SFopp (SFpred_pos (SFopp x)) end.
imports: ZArith FloatClass