def digit_lt

stelliferous@0.0.2.0 · proofs/nat_order.bend:251

import Base
import stelliferous@0.0.2.0/proofs/u32_comparison.bend as Comparison
import stelliferous@0.0.2.0/proofs/word_encoding.bend as WordEncoding

251def digit_lt(+a: Nat,+b: Nat,+bit: Bool,h: {Nat.is_lt(a,b) == True{} : Bool}) -> {Nat.is_lt(Comparison.digit(bit,a),
252    Nat.double(b)) == True{} : Bool}:
253  match a b bit:
254    case 0n 0n bit:
255      Empty.absurd({Nat.is_lt(Comparison.digit(bit,0n),0n) == True{} : Bool},WordEncoding.false_true(h))
256    case 0n 1n+b False{}:
257      {==}
258    case 0n 1n+b True{}:
259      {==}
260    case 1n+a 0n bit:
261      Empty.absurd({Nat.is_lt(Comparison.digit(bit,1n+a),0n) == True{} : Bool},WordEncoding.false_true(h))
262    case 1n+a 1n+b False{}:
263      digit_lt(a,b,False{},h)
264    case 1n+a 1n+b True{}:
265      digit_lt(a,b,True{},h)