def huge_n
bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64sh.bend:343
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64sh.bend as W64sh
import Base
import bend-collections-laws-crypto@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
343def huge_n(+x: Nat) -> {S.bit_value(Bool.not(Nat.is_eq(x, 0n))) == SW.jam(0n, x) : Nat}:
344 match x:
345 case 0n:
346 {==}
347 case 1n+n:
348 Equal.sym(Nat, SW.jam(0n, 1n+n), 1n, Equal.trans(Nat, SW.jam(0n, 1n+n), SW.jam(0n, 1n), 1n, jam_r1(0n, n), {==}))