def internal_div_go_one

bend-mathlib@0.8.1.0 · nat.bend:1872

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

import Base

1872def internal_div_go_one(a: Nat, +d: Nat) -> {(Nat.add(a, d), 0n) == Nat.divmod.go(a, 0n, d, 0n) : Nat & Nat}:
1873  match a:
1874    case 0n:
1875      {==}
1876    case 1n++p:
1877      %add_succ(p, d) : {(_, 0n) == Nat.divmod.go(p, 0n, 1n+d, 0n) : Nat & Nat}
1878      internal_div_go_one(p, 1n+d)

Uses (6)

Used by (2)