proposition: Lemma gpPtUn h k u : valid (k \-> u \+ h) -> gapless (k \-> u \+ h) -> last_key h < k -> k = fresh h.
proof: Proof. move=>V C N; apply/eqP/contraT=>X. have Y : fresh h < k by rewrite leq_eqVlt eq_sym (negbTE X) in N. suff Z : last_key (k \-> u \+ h) = k. - move: (C (fresh h)); rewrite Z (leq_eqVlt _ k) Y orbT andbT; move/(_ (erefl _)). rewrite domPtUn inE (negbTE X) /=; case/andP=>_ /dom_ordfresh. by rewrite ltnn. apply: max_lastkey (find_some (findPtUn V)) _ => x. rewrite domUn inE; case/andP=>_ /orP []. - by rewrite domPt inE; case/andP=>_ /eqP ->. by move/lastkey_max/leq_ltn_trans/(_ N)/ltnW. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)