law div_small

lawful-words@0.1.0.0 · proof_nat.bend:1105

import Base

1105law div_small:
1106  for +a: Nat
1107  for +b: Nat
1108  for +h: {Nat.is_lt(a, b) == True{} : Bool}
1109  {Nat.div(a, b) == 0n : Nat}