def AP.lt_split2

bend-osdev-array@0.1.0.1 · PROOF.bend:1014

import bend-osdev-array@0.1.0.1/PROOF.bend as PROOF

import Base
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL

1014def AP.lt_split2(+w: Nat, +s: Nat, h: {Nat.is_lt(Nat.add(s, w), Nat.double(s)) == True{} : Bool}) -> {Nat.is_lt(w, s) == True{} : Bool}:
1015  %AP.lt_cancel(s, w, s) : {_ == True{} : Bool}
1016  %UL.nat_double(s) : {Nat.is_lt(Nat.add(s, w), _) == True{} : Bool}
1017  h

Uses (7)

Used by (2)