proposition: Lemma gapless_pleq h1 h2 : gapless h1 -> valid h2 -> [pcm h1 <= h2] -> exists h, h2 = h1 \+ h /\ forall k, k \in dom h -> last_key h1 < k.
proof: Proof. move=>G V H; case: H V=>h ->{h2} V; exists h; split=>// k D. apply: contraR (dom_inNR V D)=>H; apply: G; move/dom_cond: D=>/= D. by rewrite lt0n D leqNgt. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)