U32.internal_bit_double_lt: def of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/u32.bend as U32
Lines 824-830 of bend-mathlib@0.8.1.0/u32.bend: https://jend.leeeet.dev/read.txt?path=bend-mathlib@0.8.1.0/u32.bend&start_line=824&end_line=830

import Base
import bend-mathlib@0.8.1.0/nat.bend as MNat

def internal_bit_double_lt(x: Bool, +r: Nat, +b: Nat, h: MNat.lt(r, b)) -> MNat.lt(Nat.add(internal_bv(x), Nat.double(r)), Nat.double(b)):
  match x:
    case False{}:
      MNat.double_lt_double(r, b, h)
    case True{}:
      %Equal.sym(Bool, Nat.is_lt(1n+Nat.double(r), Nat.double(b)), Nat.is_le(2n+Nat.double(r), Nat.double(b)), MNat.is_lt_eq_succ_le(1n+Nat.double(r), Nat.double(b))) : {_ == True{} : Bool}
      MNat.double_le_double(1n+r, b, MNat.succ_le_of_lt(r, b, h))

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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.double
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=double_le_double
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=double_lt_double
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=is_lt_eq_succ_le
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=lt
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=succ_le_of_lt
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/u32.bend&name=internal_bv