def un.lt_half

bend-osdev-u32@0.1.0.0 · PROOF.bend:2092

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U

2092def un.lt_half(y: Bool, +v: Nat, +d: Nat, h: {Nat.is_lt(Nat.add(U.U32Nat.bit(y), Nat.double(v)), Nat.double(d)) == True{} : Bool}) -> {Nat.is_lt(v, d) == True{} : Bool}:
2093  match y:
2094    case False{}:
2095      Equal.trans(Bool, Nat.is_lt(v, d), Nat.is_lt(Nat.double(v), Nat.double(d)), True{}, Equal.sym(Bool, Nat.is_lt(Nat.double(v), Nat.double(d)), Nat.is_lt(v, d), un.lt_dbl(v, d)), h)
2096    case True{}:
2097      Equal.trans(Bool, Nat.is_lt(v, d), Nat.is_lt(1n+Nat.double(v), Nat.double(d)), True{}, Equal.sym(Bool, Nat.is_lt(1n+Nat.double(v), Nat.double(d)), Nat.is_lt(v, d), un.lt_dbl1(v, d)), h)