law nat_div_unique

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

import Base

369law nat_div_unique:
370  for +b: Nat
371  for +q1: Nat
372  for +r1: Nat
373  for +q2: Nat
374  for +r2: Nat
375  for e: {Nat.add(Nat.mul(q1, b), r1) == Nat.add(Nat.mul(q2, b), r2) : Nat}
376  for h1: {Nat.is_lt(r1, b) == True{} : Bool}
377  for h2: {Nat.is_lt(r2, b) == True{} : Bool}
378  {q1 == q2 : Nat}