def shifted_span

stelliferous@0.0.2.0 · proofs/nat_interval.bend:14

import Base
import stelliferous@0.0.2.0/proofs/nat_order.bend as Order
import stelliferous@0.0.2.0/proofs/natural_addition.bend as Addition

14def shifted_span(+first: Nat,+rows: Nat,+begin: Nat,+end: Nat,lower: {Nat.is_le(first,begin) == True{} : Bool},
15  ordered: {Nat.is_le(begin,end) == True{} : Bool},upper: {Nat.is_le(end,Nat.add(first,rows)) == True{} : Bool}) ->
16  {Nat.is_le(Nat.add(Nat.sub(begin,first),Nat.sub(end,begin)),rows) == True{} : Bool}:
17  Order.cancel_offset_le(first,Nat.add(Nat.sub(begin,first),Nat.sub(end,begin)),rows,
18    %Addition.associative(first,Nat.sub(begin,first),Nat.sub(end,begin)) : {Nat.is_le(_,Nat.add(first,rows)) == True{} : Bool}
19    %Equal.sym(Nat,Nat.add(first,Nat.sub(begin,first)),begin,Order.restore_shift(first,begin,lower)) : {Nat.is_le(Nat.add(_,Nat.sub(end,begin)),Nat.add(first,rows)) == True{} : Bool}
20    %Equal.sym(Nat,Nat.add(begin,Nat.sub(end,begin)),end,Order.restore_shift(begin,end,ordered)) : {Nat.is_le(_,Nat.add(first,rows)) == True{} : Bool} upper)