def hlf_double

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/u32half.bend:32

import Base

32def hlf_double(+q: Nat) -> {hlf(Nat.double(q)) == q : Nat}:
33  match q:
34    case 0n:
35      {==}
36    case 1n+p:
37      Equal.cong(Nat, Nat, n => 1n+n, hlf(Nat.double(p)), p, hlf_double(p))