proposition: Lemma valid_indb (P : natmap A -> Prop) : P Unit -> (forall u, P (1 \-> u)) -> (forall t u h, P h -> last_key h < t -> valid (h \+ t \-> u) -> P (t \-> u \+ h)) -> forall h, valid h -> P h.
proof: Proof. move=>H1 H2 H3; elim/um_indb=>//=. - by rewrite -[valid _]negbK; move/negP/invalidE. move=>k v f H V K _. case E: (unitb f); last first. - apply: H3=>//; first by apply: H (validL V). apply: K; apply: contraR (negbT E). by rewrite -unitbE; apply: lastkey_dom (validL V). move/unitbE: {K H} E V=>->; rewrite unitL unitR => V. move: (H3 k v Unit H1); rewrite unitL unitR lastkey0 lt0n. by apply=>//; rewrite validPt /= in V. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)