proposition: Lemma dom_umfilt_le_eq A (h : natmap A) t1 t2 : t1 \in 0::dom h -> t2 \in 0::dom h -> um_filter (le t1) h = um_filter (le t2) h -> t1 = t2.
proof: Proof. rewrite !inE; case/orP=>[/eqP ->|/In_domX [v1 T1]]. - case/orP=>[/eqP ->|/In_domX [v2 T2]] //. move/eq_in_umfilt=>/(_ (t2, v2) T2) /=. by rewrite leqnn leqn0 eq_sym=>/eqP. case/orP=>[/eqP ->|/In_domX [v2 T2] L]. - move/eq_in_umfilt=>/(_ (t1, v1) T1) /=. by rewrite leqnn leqn0=>/esym/eqP. move/eq_in_umfilt: (L)=>/(_ (t1, v1) T1). move/eq_in_umfilt: (L)=>/(_ (t2, v2) T2) /=. by rewrite !leqnn; case: ltngtP. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)