fact: Definition SFabs x := match x with | S754_nan => S754_nan | S754_infinity sx => S754_infinity false | S754_finite sx mx ex => S754_finite false mx ex | S754_zero sx => S754_zero false end.
imports: ZArith FloatClass