def internal_bit_double_lt

bend-mathlib@0.8.1.0 · u32.bend:824

import Base
import bend-mathlib@0.8.1.0/nat.bend as MNat

824def internal_bit_double_lt(x: Bool, +r: Nat, +b: Nat, h: MNat.lt(r, b)) -> MNat.lt(Nat.add(internal_bv(x), Nat.double(r)), Nat.double(b)):
825  match x:
826    case False{}:
827      MNat.double_lt_double(r, b, h)
828    case True{}:
829      %Equal.sym(Bool, Nat.is_lt(1n+Nat.double(r), Nat.double(b)), Nat.is_le(2n+Nat.double(r), Nat.double(b)), MNat.is_lt_eq_succ_le(1n+Nat.double(r), Nat.double(b))) : {_ == True{} : Bool}
830      MNat.double_le_double(1n+r, b, MNat.succ_le_of_lt(r, b, h))