def bit_or_le

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/xbits.bend:110

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

110# or never exceeds the sum
111def bit_or_le(+a: Bool, +b: Bool) -> {Nat.is_le(SN.bit_value(Bool.or(a, b)), Nat.add(SN.bit_value(a), SN.bit_value(b))) == True{} : Bool}:
112  match a b:
113    case True{} True{}:
114      {==}
115    case True{} False{}:
116      {==}
117    case False{} True{}:
118      {==}
119    case False{} False{}:
120      {==}