is 2^e <= N/M ? with e = eOffset - specOffset (either sign)
133def specPowerFits =
134 (lambda unrestricted numerator : Nat . (lambda unrestricted denominator : Nat . (lambda unrestricted eOffset : Nat .
135 (nat-eliminate (lambda unrestricted current : Nat . Nat)
136 (specLessOrEqual denominator (nat-multiply numerator (specPow2 (nat-subtract specOffset eOffset))))
137 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat .
138 (specLessOrEqual (nat-multiply denominator (specPow2 (nat-subtract eOffset specOffset))) numerator)))
139 (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.