Hash.and_le: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/hash/hash.bend as Hash
Lines 30-36 of bend-collections-laws-math@1.0.0.0/proofs/math/hash/hash.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/hash/hash.bend&start_line=30&end_line=36

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD

# masking never exceeds the mask
def and_le(+n: Nat, +x: Word(n), +m: Word(n)) -> {Nat.is_le(WD.uw(n, Word.and(n, x, m)), WD.uw(n, m)) == True{} : Bool}:
  match n x m:
    case 0n WNil{} WNil{}:
      {==}
    case 1n+p WCon{a, t1} WCon{b, t2}:
      add_le(S.bit_value(Bool.and(a, b)), S.bit_value(b), Nat.double(WD.uw(p, Word.and(p, t1, t2))), Nat.double(WD.uw(p, t2)), bit_and_le(a, b), N.double_le(WD.uw(p, Word.and(p, t1, t2)), WD.uw(p, t2), and_le(p, t1, t2)))

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  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=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Nil
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.and
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend&name=bit_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=double_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=uw
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/hash/hash.bend&name=add_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/hash/hash.bend&name=bit_and_le