proposition: Lemma valid_indf (P : natmap A -> Prop) : P Unit -> (forall t u h, P h -> (forall x, x \in dom h -> t < x) -> valid (t \-> u \+ h) -> P (t \-> u \+ h)) -> forall h, valid h -> P h.
proof: Proof. move=>H1 H2; elim/um_indf=>//=. - by rewrite -[valid _]negbK; move/negP/invalidE. move=>k v f H V K _. apply: H2=>//; first by apply: H (validR V). move=>x; move/(order_path_min (@ordtype.trans _)): K. by case: allP=>// X _; apply: X. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)