def AP.lt_split

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

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

808# a value below double(s), split at s
809def AP.lt_split(+w: Nat, +s: Nat, h: {Nat.is_lt(Nat.add(w, s), Nat.double(s)) == True{} : Bool}) -> {Nat.is_lt(w, s) == True{} : Bool}:
810  %AP.lt_cancel(s, w, s) : {_ == True{} : Bool}
811  %UL.nat_add_comm(w, s) : {Nat.is_lt(_, Nat.add(s, s)) == True{} : Bool}
812  %UL.nat_double(s) : {Nat.is_lt(Nat.add(w, s), _) == True{} : Bool}
813  h