proposition: Lemma umfilt_le_gapless A (h1 h2 : natmap A) t : gapless h1 -> valid h2 -> [pcm h1 <= h2] -> t <= last_key h1 -> um_filter (le t) h2 = um_filter (le t) h1.
proof: Proof. move=>G V H K; case: (gapless_pleq G V H)=>h [? D]. by subst h2; rewrite umfilt_leUn. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)