def bit_double_lt

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/nat.bend:401

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S

401# bit + 2u < 2v gives u < v.
402def bit_double_lt(+b: Bool, +u: Nat, +v: Nat, e: {Nat.is_lt(Nat.add(S.bit_value(b), Nat.double(u)), Nat.double(v)) == True{} : Bool}) -> {Nat.is_lt(u, v) == True{} : Bool}:
403  match b u v:
404    case _ _ 0n:
405      Empty.absurd({Nat.is_lt(u, 0n) == True{} : Bool}, lt_zero_absurd(Nat.add(S.bit_value(b), Nat.double(u)), e))
406    case _ 0n 1n+q:
407      {==}
408    case False{} 1n+p 1n+q:
409      bit_double_lt(False{}, p, q, e)
410    case True{} 1n+p 1n+q:
411      bit_double_lt(True{}, p, q, e)