proposition: Lemma dom_freshUn h1 h2 : valid h1 -> [pcm h2 <= h1] -> fresh h1 \notin dom h2.
proof: Proof. move=>V [x E]; rewrite {h1}E in V *; apply: contra (@dom_ordfresh _ _) _. by rewrite joinC in V *; rewrite -leqNgt; apply: lastkeyUnf. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)