def cbit_one

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/bitsv.bend:145

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/semiring.bend as SR

145# (1 - b) one + b one = one
146def cbit_one(+one: Nat, +b: Nat, +hb: {Nat.is_lt(b, 2n) == True{} : Bool}) -> {Nat.add(Nat.mul(Nat.sub(1n, b), one), Nat.mul(b, one)) == one : Nat}:
147  %Equal.sym(Nat, Nat.add(Nat.mul(Nat.sub(1n, b), one), Nat.mul(b, one)), Nat.mul(Nat.add(Nat.sub(1n, b), b), one), Equal.sym(Nat, Nat.mul(Nat.add(Nat.sub(1n, b), b), one), Nat.add(Nat.mul(Nat.sub(1n, b), one), Nat.mul(b, one)), NA.mul_add_right(Nat.sub(1n, b), b, one))) : {_ == one : Nat}
148  %Equal.sym(Nat, Nat.add(Nat.sub(1n, b), b), 1n, cbit(b, hb)) : {Nat.mul(_, one) == one : Nat}
149  SR.one_mul(one)