law go_lt

lawful-words@0.1.0.0 · proof_nat.bend:985

import Base

985law go_lt:
986  for +n: Nat
987  for +m: Nat
988  for +d: Nat
989  for +r: Nat
990  for +bp: Nat
991  for +h: {Nat.add(m, r) == bp : Nat}
992  {Nat.is_lt(Pair.snd(Nat, Nat, Nat.divmod.go(n, m, d, r)), 1n+bp) == True{} : Bool}