def same

bend-collections-laws-crypto@1.0.0.0 · proofs/math/pow2/pow2.bend:15

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/src/math/pow2.bend as P

15def same(+d: Nat) -> {P.pow2t(d) == SC.pow2(d) : Nat}:
16  match d:
17    case 0n:
18      {==}
19    case 1n+ +p:
20      Equal.trans(Nat, P.go(p, 2n), Nat.double(P.go(p, 1n)), SC.pow2(1n+p), go_double(p, 1n), Equal.cong(Nat, Nat, Nat.double, P.go(p, 1n), SC.pow2(p), same(p)))