def uq.hk1
bend-osdev-algo@0.1.0.0 · proof_u32.bend:401
import bend-osdev-algo@0.1.0.0/proof_u32.bend as ProofU32
import Base
401def uq.hk1(+s2: Nat, -d: Nat, +q: Nat, e: {Nat.double(s2) == d : Nat}, h: {Nat.is_lt(1n+d, Nat.double(q)) == True{} : Bool}) -> {Nat.is_lt(s2, q) == True{} : Bool}:
402 Equal.trans(Bool, Nat.is_lt(s2, q), Nat.is_lt(1n+Nat.double(s2), Nat.double(q)), True{}, Equal.sym(Bool, Nat.is_lt(1n+Nat.double(s2), Nat.double(q)), Nat.is_lt(s2, q), uq.lt_dbl1(s2, q)), uq.lt_rw(1n+d, 1n+Nat.double(s2), Nat.double(q), uq.succ_cong(d, Nat.double(s2), Equal.sym(Nat, Nat.double(s2), d, e)), h))