Fround.R_le: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend as Fround
Lines 247-251 of bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend&start_line=247&end_line=251

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH

def R_le(+one: Nat, +h1: {one == 1n : Nat}, +m: Nat, +hm: {C.fits(63n, m) == True{} : Bool}) -> {Nat.is_le(Nat.add(C.high(10n, m), C.high(10n, Nat.add(C.low(10n, m), 512n))), C.shift(53n, one)) == True{} : Bool}:
  +t = C.high(10n, Nat.add(C.low(10n, m), 512n))
  +ht = le1(t, SH.fits_high(10n, 1n, Nat.add(C.low(10n, m), 512n), fits_add1(10n, C.low(10n, m), 512n, WW.low_fits(10n, m), {==})))
  +hq = WW.lt_one(53n, one, h1, C.high(10n, m), SH.fits_high(10n, 53n, m, hm))
  N.le_trans(Nat.add(C.high(10n, m), C.high(10n, Nat.add(C.low(10n, m), 512n))), Nat.add(C.high(10n, m), 1n), C.shift(53n, one), N.le_add_left(t, 1n, C.high(10n, m), ht), succ_le(C.high(10n, m), C.shift(53n, one), hq))

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=le_add_left
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=le_trans
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend&name=fits_add1
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend&name=le1
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend&name=succ_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend&name=fits_high
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=low_fits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=lt_one
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=fits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=high
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=low
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift