1	# The same binary-digit interpretation serves long division and division by two.
2	import Base
3	import ./u32_comparison.bend as Comparison
4	
5	def word_digit(+n: Nat,+bit: Bool,+w: Word(n)) -> {Word.to_nat(1n+n,WCon{bit,w}) == Comparison.digit(bit,Word.to_nat(n,w)) : Nat}:
6	  match bit:
7	    case False{}:
8	      {==}
9	    case True{}:
10	      {==}