fact: Definition ix_bnd {A : eqType} (s : seq A) (i : itv_bound A) : itv_bound nat := match i with | BSide b x => BSide b (index x s) | BInfty b => BInfty _ b end.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)