proposition: Lemma gp_fresh h u : gapless (fresh h \-> u \+ h) <-> gapless h.
proof: Proof. case V : (valid h); last first. - by move/invalidE: (negbT V)=>->; rewrite join_undef. split=>H k; move: (V); rewrite -(valid_fresh u (leqnn _))=>V'; last first. - rewrite lastkey_fresh // domPtUn inE V' /= (leq_eqVlt k) eq_sym. by move: (H k); rewrite -(ltnS k); case: (ltngtP k (last_key h).+1). rewrite -(ltnS k) -/(fresh h); case/andP=>Z N. move: (H k); rewrite lastkey_fresh // domPtUn inE V' Z /= leq_eqVlt eq_sym. by case: ltngtP N=>//= _ _; apply. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)