Nat.internal_div_le_step: def of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/nat.bend as Nat
Lines 934-939 of bend-mathlib@0.8.1.0/nat.bend: https://jend.leeeet.dev/read.txt?path=bend-mathlib@0.8.1.0/nat.bend&start_line=934&end_line=939

import Base

def internal_div_le_step(+np: Nat, +a: Nat, +bp: Nat, b: Bool, eb: {b == Nat.is_le(1n+bp, a) : Bool}, ih: @x:Nat -> {Nat.is_le(np, Nat.div(x, 1n+bp)) == Nat.is_le(Nat.mul(np, 1n+bp), x) : Bool}) -> {Nat.is_le(1n+np, Nat.div(a, 1n+bp)) == Nat.is_le(Nat.mul(1n+np, 1n+bp), a) : Bool}:
  match b:
    case True{}:
      internal_div_le_big(np, a, bp, internal_div_le_wit(1n+bp, a, Equal.sym(Bool, True{}, Nat.is_le(1n+bp, a), eb)), ih)
    case False{}:
      internal_div_le_small(np, a, bp, internal_div_le_wit(a, bp, internal_div_not_succ_le(a, bp, eb)))

Uses (10):
  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.div
  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.mul
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=internal_div_le_big
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=internal_div_le_small
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=internal_div_le_wit
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=internal_div_not_succ_le