law carry_mod

lawful-words@0.1.0.0 · proof_word.bend:146

import Base

146# r + c * m = x with r < m gives x % m = r.
147law carry_mod:
148  for +r: Nat
149  for +c: Nat
150  for +m: Nat
151  for +x: Nat
152  for +e: {Nat.add(r, Nat.mul(c, m)) == x : Nat}
153  for +h: {Nat.is_lt(r, m) == True{} : Bool}
154  {Nat.mod(x, m) == r : Nat}