~/jendhub

def internal_div_block_step

bend-mathlib@0.8.1.0 · nat.bend:757

import bend-mathlib@0.8.1.0/nat.bend as Nat
import Base

757def internal_div_block_step(-bp: Nat, r: Nat, -mp: Nat, h: {bp == Nat.add(r, 1n+mp) : Nat}) -> {bp == 1n+Nat.add(r, mp) : Nat}:
758  %add_succ(r, mp) : {bp == _ : Nat}
759  h

Uses (3)

Used by (1)