proposition: Lemma find_fresh h x : fresh h <= x -> find x h = None.
proof: Proof. by move=>H; rewrite In_findNE // ordfresh_dom. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)