def double_lt_bit

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

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

413def double_lt_bit(+b: Bool, +u: Nat, +v: Nat, e: {Nat.is_lt(u, v) == True{} : Bool}) -> {Nat.is_lt(Nat.add(S.bit_value(b), Nat.double(u)), Nat.double(v)) == True{} : Bool}:
414  match b u v:
415    case _ _ 0n:
416      Empty.absurd({Nat.is_lt(Nat.add(S.bit_value(b), Nat.double(u)), 0n) == True{} : Bool}, lt_zero_absurd(u, e))
417    case False{} 0n 1n+q:
418      {==}
419    case True{} 0n 1n+q:
420      {==}
421    case False{} 1n+p 1n+q:
422      double_lt_bit(False{}, p, q, e)
423    case True{} 1n+p 1n+q:
424      double_lt_bit(True{}, p, q, e)