law mod_small

lawful-words@0.1.0.0 · proof_nat.bend:1096

import Base

1096law mod_small:
1097  for +a: Nat
1098  for +b: Nat
1099  for +h: {Nat.is_lt(a, b) == True{} : Bool}
1100  {Nat.mod(a, b) == a : Nat}