law mod_mul_add

lawful-words@0.1.0.0 · proof_nat.bend:1083

import Base

1083law mod_mul_add:
1084  for +q: Nat
1085  for +b: Nat
1086  for +r: Nat
1087  for +h: {Nat.is_lt(r, b) == True{} : Bool}
1088  {Nat.mod(Nat.add(Nat.mul(q, b), r), b) == r : Nat}