law digits

stelliferous@0.0.2.0 · proofs/u32_comparison.bend:10

import Base

10law digits:
11  for +a: Nat
12  for +b: Nat
13  for +ab: Bool
14  for +bb: Bool
15  {Nat.cmp(digit(ab,a),digit(bb,b)) == Word.cmp.fin(ab,bb,Nat.cmp(a,b)) : Cmp}