def shifted_inside

stelliferous@0.0.2.0 · proofs/nat_interval.bend:7

import Base
import stelliferous@0.0.2.0/proofs/nat_order.bend as Order
import stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend as Bounds

7def shifted_inside(+begin: Nat,+end: Nat,+query: Nat,+lower: {Nat.is_le(begin,query) == True{} : Bool},+upper: {Nat.is_lt(query,end) == True{} : Bool}) ->
8  {Nat.is_lt(Nat.sub(query,begin),Nat.sub(end,begin)) == True{} : Bool}:
9  +ordered = Bounds.strict_le(begin,end,Order.le_lt_trans(begin,query,end,lower,upper))
10  Order.cancel_offset_lt(begin,Nat.sub(query,begin),Nat.sub(end,begin),
11    %Equal.sym(Nat,Nat.add(begin,Nat.sub(query,begin)),query,Order.restore_shift(begin,query,lower)) : {Nat.is_lt(_,Nat.add(begin,Nat.sub(end,begin))) == True{} : Bool}
12    %Equal.sym(Nat,Nat.add(begin,Nat.sub(end,begin)),end,Order.restore_shift(begin,end,ordered)) : {Nat.is_lt(query,_) == True{} : Bool} upper)