proposition: Lemma valid_freshX h1 h2 v : valid h1 -> last_key h2 <= last_key h1 -> valid (fresh h1 \-> v \+ h2) = valid h2.
proof: Proof. move=>V N; rewrite validPtUn /=; case W : (valid h2)=>//=. apply/negP=>/dom_ordfresh; rewrite ltnS /fresh. by case: ltngtP N. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)