fact: Definition gaplessb h := all (fun t => t \in dom h) (iota 1 (last_key h)).
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)