~/jendhub

def hlf_double_succ

bend-collections-laws-math@1.0.0.0 · proofs/lib/u32half.bend:39

import bend-collections-laws-math@1.0.0.0/proofs/lib/u32half.bend as U32half
import Base

39def hlf_double_succ(+q: Nat) -> {hlf(1n+Nat.double(q)) == q : Nat}:
40  match q:
41    case 0n:
42      {==}
43    case 1n+p:
44      Equal.cong(Nat, Nat, n => 1n+n, hlf(1n+Nat.double(p)), p, hlf_double_succ(p))

Uses (4)

Used by (1)