proposition: Lemma gaplessP h : reflect (gapless h) (gaplessb h).
proof: Proof. case V: (gaplessb h);constructor; last first. - move=>H;apply/(elimF idP V)/allP=>?. by rewrite mem_iota add1n ltnS=>?; apply/H. by move/allP:V=>H t;move: (H t);rewrite mem_iota add1n ltnS. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)