F64divv.lt2x: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divv.bend as F64divv
Lines 82-83 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divv.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divv.bend&start_line=82&end_line=83

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

def lt2x(+one: Nat, +h1: {one == 1n : Nat}, +n: Nat, +m: Nat, +hn: {C.fits(53n, n) == True{} : Bool}, +hm: {C.fits(52n, m) == False{} : Bool}) -> {Nat.is_lt(n, Nat.add(m, m)) == True{} : Bool}:
  N.lt_le_trans(n, C.shift(53n, one), Nat.add(m, m), hi53(one, h1, n, hn), dbl53(one, h1, m, hm))

Uses (9):
  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_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=lt_le_trans
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divv.bend&name=dbl53
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divv.bend&name=hi53
  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=shift