law nat_div_small

lawful-words@0.1.0.0 · LAWS.bend:485

import Base

485law nat_div_small:
486  for a: Nat
487  for b: Nat
488  for h: {Nat.is_lt(a, b) == True{} : Bool}
489  {Nat.div(a, b) == 0n : Nat}