def internal_mod_go_le

bend-mathlib@0.8.1.0 · nat.bend:1930

import Base

1930def internal_mod_go_le(n: Nat, m: Nat, -d: Nat, +r: Nat) -> le(Pair.snd(Nat, Nat, Nat.divmod.go(n, m, d, r)), Nat.add(r, m)):
1931  match n m:
1932    case 0n k:
1933      le_add_right(r, k)
1934    case 1n++np 0n:
1935      %internal_div_add_zero_r(r) : le(Pair.snd(Nat, Nat, Nat.divmod.go(np, r, 1n+d, 0n)), _)
1936      internal_mod_go_le(np, r, 1n+d, 0n)
1937    case 1n++np 1n++mp:
1938      %Equal.sym(Nat, Nat.add(r, 1n+mp), 1n+Nat.add(r, mp), add_succ(r, mp)) : le(Pair.snd(Nat, Nat, Nat.divmod.go(np, mp, d, 1n+r)), _)
1939      internal_mod_go_le(np, mp, d, 1n+r)