law min_le4

lawful-bytes@0.1.1.0 · proof_fast_find2.bend:110

import Base
import lawful-bytes@0.1.1.0/proof_fast_word.bend as FW

110law min_le4:
111  for +v1: U32
112  for +v2: U32
113  {Nat.is_le(Nat.min(FW.P0(v1), FW.P0(v2)), 4n) == True{} : Bool}