def uq.hk3

bend-osdev-algo@0.1.0.0 · proof_u32.bend:407

import Base

407def uq.hk3(+s2: Nat, -d: Nat, +q: Nat, e: {Nat.double(s2) == d : Nat}, h: {Nat.is_lt(3n+d, Nat.double(q)) == True{} : Bool}) -> {Nat.is_lt(1n+s2, q) == True{} : Bool}:
408  Equal.trans(Bool, Nat.is_lt(1n+s2, q), Nat.is_lt(1n+Nat.double(1n+s2), Nat.double(q)), True{}, Equal.sym(Bool, Nat.is_lt(1n+Nat.double(1n+s2), Nat.double(q)), Nat.is_lt(1n+s2, q), uq.lt_dbl1(1n+s2, q)), uq.lt_rw(3n+d, 3n+Nat.double(s2), Nat.double(q), uq.succ_cong(2n+d, 2n+Nat.double(s2), uq.succ_cong(1n+d, 1n+Nat.double(s2), uq.succ_cong(d, Nat.double(s2), Equal.sym(Nat, Nat.double(s2), d, e)))), h))