law div_uniq

lawful-words@0.1.0.0 · proof_nat.bend:1033

import Base

1033# q1 * b + r1 = q2 * b + r2 with r1, r2 < b gives q1 = q2.
1034law div_uniq:
1035  for +q1: Nat
1036  for +q2: Nat
1037  for +b: Nat
1038  for +r1: Nat
1039  for +r2: Nat
1040  for h1: {Nat.is_lt(r1, b) == True{} : Bool}
1041  for h2: {Nat.is_lt(r2, b) == True{} : Bool}
1042  for e: {Nat.add(Nat.mul(q1, b), r1) == Nat.add(Nat.mul(q2, b), r2) : Nat}
1043  {q1 == q2 : Nat}