law n_mod_lt

lawful-arrays@0.1.0.0 · proof_words.bend:62

import Base

62law n_mod_lt:
63  for +a: Nat
64  for +b: Nat
65  for +h: {Nat.is_lt(0n, b) == True{} : Bool}
66  {Nat.is_lt(Nat.mod(a, b), b) == True{} : Bool}