def internal_div_go_d_ge
bend-mathlib@0.8.1.0 · nat.bend:832
import bend-mathlib@0.8.1.0/nat.bend as Nat
import Base
832def internal_div_go_d_ge(+j: Nat, n: Nat, m: Nat, +d: Nat, r: Nat, h: {True{} == Nat.is_le(j, d) : Bool}) -> {True{} == Nat.is_le(j, Pair.fst(Nat, Nat, Nat.divmod.go(n, m, d, r))) : Bool}:
833 match n m:
834 case 0n _:
835 h
836 case 1n+np 0n:
837 internal_div_go_d_ge(j, np, r, 1n+d, 0n, internal_div_le_succ_r(j, d, h))
838 case 1n+np 1n+mp:
839 internal_div_go_d_ge(j, np, mp, d, 1n+r, h)