proposition: Lemma omf_path h : path ltn 0 (dom (f h)).
proof: Proof. rewrite path_min_sorted; first by apply: omf_sorted. by apply/allP=>z /dom_cond /=; case: z. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)