law hh_le

lawful-bytes@0.1.1.0 · proof_fast_append.bend:1291

import Base

1291law hh_le:
1292  for +ld: U32
1293  for +n: U32
1294  {Nat.is_le(U32.to_nat(HH(ld, n)), U32.to_nat(n)) == True{} : Bool}