ProofU32.div_if_ok: def of lawful-words@0.1.0.0
Import: import lawful-words@0.1.0.0/proof_u32.bend as ProofU32
Lines 843-852 of lawful-words@0.1.0.0/proof_u32.bend: https://jend.leeeet.dev/read.txt?path=lawful-words@0.1.0.0/proof_u32.bend&start_line=843&end_line=852

import Base
import lawful-words@0.1.0.0/proof_nat.bend as N

def div_if_ok(+x: Word(32n), +y: Word(32n), +m: Nat, +hm: {Nat.pow(2n, 32n) == m : Nat}, z: Bool, +ez: {U32.is_zero(U32{y}) == z : Bool}) ->
  {U32.to_nat(U32.div.if(x, U32{y}, z)) == Nat.div(Word.to_nat(32n, x), Word.to_nat(32n, y)) : Nat}:
  match z:
    case True{}:
      %Equal.sym(Nat, Word.to_nat(32n, y), 0n, N.eq_sound(Word.to_nat(32n, y), 0n, %is_zero_to_nat(U32{y}) : {_ == True{} : Bool}; ez)) :
        {0n == Nat.div(Word.to_nat(32n, x), _) : Nat}
      {==}
    case False{}:
      div_fin_ok(Word.to_nat(32n, x), Word.to_nat(32n, y), U32.divmod.go(32n, x, U32{y}),
        dm_ok(32n, x, U32{y}, ne_zero_pos(Word.to_nat(32n, y), %is_zero_to_nat(U32{y}) : {_ == False{} : Bool}; ez), m, hm))

Uses (17):
  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.pow
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.div.if
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.divmod.go
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_zero
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.to_nat
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=eq_sound
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_u32.bend&name=div_fin_ok
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_u32.bend&name=dm_ok
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_u32.bend&name=is_zero_to_nat
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_u32.bend&name=ne_zero_pos