is 2^e <= N/M ? with e = eOffset - specOffset (either sign)
136def specPowerFits =
137 (lambda unrestricted numerator : Nat . (lambda unrestricted denominator : Nat . (lambda unrestricted eOffset : Nat .
138 (nat-eliminate (lambda unrestricted current : Nat . Nat)
139 (specLessOrEqual denominator (nat-multiply numerator (specPow2 (nat-subtract specOffset eOffset))))
140 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat .
141 (specLessOrEqual (nat-multiply denominator (specPow2 (nat-subtract eOffset specOffset))) numerator)))
142 (specLessOrEqual specOffset eOffset)))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.