def div2_step

bend-collections-laws-math@1.0.0.0 · proofs/lib/nat.bend:510

import Base

510def div2_step(+i: Nat) -> {Nat.div(Nat.add(2n, i), 2n) == 1n+Nat.div(i, 2n) : Nat}:
511  Equal.trans(Nat, Pair.fst(Nat, Nat, Nat.divmod.go(Nat.add(2n, i), 1n, 0n, 0n)), Pair.fst(Nat, Nat, bump2(Nat.divmod.go(i, 1n, 0n, 0n))), 1n+Pair.fst(Nat, Nat, Nat.divmod.go(i, 1n, 0n, 0n)),
512    Equal.cong(Nat & Nat, Nat, pq => Pair.fst(Nat, Nat, pq), Nat.divmod.go(Nat.add(2n, i), 1n, 0n, 0n), bump2(Nat.divmod.go(i, 1n, 0n, 0n)),
513      Equal.trans(Nat & Nat, Nat.divmod.go(Nat.add(2n, i), 1n, 0n, 0n), Nat.divmod.go(i, 1n, 1n, 0n), bump2(Nat.divmod.go(i, 1n, 0n, 0n)),
514        peel2(i, 0n), acc2(i, 1n, 0n, 0n))),
515    fst_bump2(Nat.divmod.go(i, 1n, 0n, 0n)))