def internal_div_block_start

bend-mathlib@0.8.1.0 · nat.bend:753

import Base

753def internal_div_block_start(-bp: Nat, +r: Nat, h: {bp == Nat.add(r, 0n) : Nat}) -> {bp == r : Nat}:
754  %add_zero(r) : {bp == _ : Nat}
755  h