proposition: Lemma umcnt_le_gapless A p (h1 h2 : natmap A) t : gapless h1 -> valid h2 -> [pcm h1 <= h2] -> t <= last_key h1 -> um_count (predI p (le t)) h2 = um_count (predI p (le t)) h1.
proof: Proof. by move=>G V K D; rewrite -!umcnt_umfilt (umfilt_le_gapless G). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)