ProofU32.shln_mod.go: def of lawful-words@0.1.0.0
Import: import lawful-words@0.1.0.0/proof_u32.bend as ProofU32
Lines 1088-1109 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=1088&end_line=1109

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

def shln_mod.go(+x: Nat, +k: Nat, +m: Nat, +hm: {Nat.pow(2n, 32n) == m : Nat}, z: Bool, +ez: {Nat.is_le(k, 32n) == z : Bool}) ->
  {Nat.mod(Nat.mod(Nat.mul(x, Nat.pow(2n, k)), m), Nat.pow(2n, k)) == 0n : Nat}:
  match z:
    case True{}:
      %hm : {Nat.mod(Nat.mod(Nat.mul(x, Nat.pow(2n, k)), _), Nat.pow(2n, k)) == 0n : Nat}
      %Equal.sym(Nat, Nat.mod(Nat.mod(Nat.mul(x, Nat.pow(2n, k)), Nat.pow(2n, 32n)), Nat.pow(2n, k)), Nat.mod(Nat.mul(x, Nat.pow(2n, k)), Nat.pow(2n, k)),
          N.mod_mod_pow(Nat.mul(x, Nat.pow(2n, k)), k, 32n, ez)) :
        {_ == 0n : Nat}
      N.mul_mod(x, Nat.pow(2n, k))
    case False{}:
      +d = Nat.sub(k, 32n)
      +pd = Nat.pow(2n, d)
      +inner = {
        %N.le_sub_add(32n, k, N.lt_to_le(32n, k, N.not_le_lt(k, 32n, ez))) : {Nat.mod(Nat.mul(x, Nat.pow(2n, _)), m) == 0n : Nat}
        %Equal.sym(Nat, Nat.pow(2n, Nat.add(32n, d)), Nat.mul(Nat.pow(2n, 32n), pd), N.pow_add(2n, 32n, d)) :
          {Nat.mod(Nat.mul(x, _), m) == 0n : Nat}
        %Equal.sym(Nat, Nat.pow(2n, 32n), m, hm) : {Nat.mod(Nat.mul(x, Nat.mul(_, pd)), m) == 0n : Nat}
        %N.mul_comm(pd, m) : {Nat.mod(Nat.mul(x, _), m) == 0n : Nat}
        %N.mul_assoc(x, pd, m) : {Nat.mod(_, m) == 0n : Nat}
        N.mul_mod(Nat.mul(x, pd), m) : {Nat.mod(Nat.mul(x, Nat.pow(2n, k)), m) == 0n : Nat}}
      %Equal.sym(Nat, Nat.mod(Nat.mul(x, Nat.pow(2n, k)), m), 0n, inner) : {Nat.mod(_, Nat.pow(2n, k)) == 0n : Nat}
      N.mod_zero_l(Nat.pow(2n, k))

Uses (18):
  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.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.pow
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=le_sub_add
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=lt_to_le
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=mod_mod_pow
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=mod_zero_l
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=mul_assoc
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=mul_comm
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=mul_mod
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=not_le_lt
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=pow_add