proposition: Lemma umfilt_le0 A (h : natmap A) t : valid h -> {in dom h, forall k, t < k} -> um_filter (le t) h = Unit.
proof: Proof. move=>V D; rewrite -(umfilt_pred0 V). apply/eq_in_umfilt; case=>k v [/= _][z E]; subst h. rewrite leqNgt; apply: contraTF (D k _)=>//. by rewrite domPtUn inE V eqxx. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)