def internal_div_go_self

bend-mathlib@0.8.1.0 · nat.bend:1900

import Base

1900def internal_div_go_self(m: Nat, -d: Nat, -r: Nat) -> {(1n+d, 0n) == Nat.divmod.go(1n+m, m, d, r) : Nat & Nat}:
1901  match m:
1902    case 0n:
1903      {==}
1904    case 1n+p:
1905      internal_div_go_self(p, d, 1n+r)