law nat_mod_unique

bend-osdev-u32@0.1.0.0 · LAWS.bend:380

import Base

380law nat_mod_unique:
381  for +b: Nat
382  for +q1: Nat
383  for +r1: Nat
384  for +q2: Nat
385  for +r2: Nat
386  for e: {Nat.add(Nat.mul(q1, b), r1) == Nat.add(Nat.mul(q2, b), r2) : Nat}
387  for h1: {Nat.is_lt(r1, b) == True{} : Bool}
388  for h2: {Nat.is_lt(r2, b) == True{} : Bool}
389  {r1 == r2 : Nat}