proposition: Lemma omf0 h : 0 \in dom (f h) = false.
proof: Proof. by apply/negP=>/dom_cond. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)