law mod_add_mod_r

lawful-words@0.1.0.0 · proof_nat.bend:1231

import lawful-words@0.1.0.0/proof_nat.bend as ProofNat
import Base

1231law mod_add_mod_r:
1232  for +v: Nat
1233  for +u: Nat
1234  for +m: Nat
1235  {Nat.mod(Nat.add(v, Nat.mod(u, m)), m) == Nat.mod(Nat.add(v, u), m) : Nat}

Uses (5)

Used by (2)