fact: Definition shl_itv (i : interval nat) (n : nat) := let: Interval l u := i in Interval (shl_bnd l n) (shl_bnd u n).
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)