law mod_lt

lawful-words@0.1.0.0 · proof_nat.bend:1020

import Base

1020law mod_lt:
1021  for +a: Nat
1022  for +b: Nat
1023  for h: {Nat.is_lt(0n, b) == True{} : Bool}
1024  {Nat.is_lt(Nat.mod(a, b), b) == True{} : Bool}