proposition: Lemma gaplessPtUnE u2 u1 h k : gapless (k \-> u1 \+ h) <-> gapless (k \-> u2 \+ h).
proof: Proof. rewrite /gapless (lastkeyPtUnE u2); split=>H t /H; by rewrite !domPtUn !inE !validPtUn. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)