def pow2_scale

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/u32.bend:21

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

21def pow2_scale(+k: Nat) -> {SC.pow2(k) == S.scale_binary(k, 1n) : Nat}:
22  match k:
23    case 0n:
24      {==}
25    case 1n+p:
26      Equal.cong(Nat, Nat, Nat.double, SC.pow2(p), S.scale_binary(p, 1n), pow2_scale(p))