law mod_add_mod_l

lawful-words@0.1.0.0 · proof_nat.bend:1216

import Base

1216# Remainders inside sums and products.
1217law mod_add_mod_l:
1218  for +u: Nat
1219  for +v: Nat
1220  for +m: Nat
1221  {Nat.mod(Nat.add(Nat.mod(u, m), v), m) == Nat.mod(Nat.add(u, v), m) : Nat}