fact: Definition shl_bnd (i : itv_bound nat) (n : nat) := match i with | BSide b m => if (m < n)%N then -oo else BSide b (m - n) | BInfty b => BInfty _ b end.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)