law mod_add_mod_r
import lawful-words@0.1.0.0/proof_nat.bend as ProofNatimport 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}
import lawful-words@0.1.0.0/proof_nat.bend as ProofNatimport 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}