fact: Definition SFcompare f1 f2 := match f1, f2 with | S754_nan , _ | _, S754_nan => None | S754_infinity s1, S754_infinity s2 => Some match s1, s2 with | true, true => Eq | false, false => Eq | true, false => Lt | false, true => Gt end | S754_infinity s, _ => Some (if s then Lt else Gt) | _, S754_infinity s => Some (if s then Gt else Lt) | S754_finite s _ _, S754_zero _ => Some (if s then Lt else Gt) | S754_zero _, S754_finite s _ _ => Some (if s then Gt else Lt) | S754_zero _, S754_zero _ => Some Eq | S754_finite s1 m1 e1, S754_finite s2 m2 e2 => Some match s1, s2 with | true, false => Lt | false, true => Gt | false, false => match Z.compare e1 e2 with | Lt => Lt | Gt => Gt | Eq => Pcompare m1 m2 Eq end | true, true => match Z.compare e1 e2 with | Lt => Gt | Gt => Lt | Eq => CompOpp (Pcompare m1 m2 Eq) end end end.
imports: ZArith FloatClass