def bit_and_le

bend-collections-laws-math@1.0.0.0 · proofs/math/hash/hash.bend:14

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

14def bit_and_le(+a: Bool, +b: Bool) -> {Nat.is_le(S.bit_value(Bool.and(a, b)), S.bit_value(b)) == True{} : Bool}:
15  match a b:
16    case True{} True{}:
17      {==}
18    case True{} False{}:
19      {==}
20    case False{} True{}:
21      {==}
22    case False{} False{}:
23      {==}