fact: Definition mag (x : type) := match x with | Fnan => exponent_zero | Float m e => match mantissa_sign m with | Mzero => e | Mnumber _ m => exponent_add e (mantissa_digits m) end end.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig