fact: Definition scale (f : type) d := match f with | Float m e => Float m (exponent_add e d) | _ => f end.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig