proposition: Lemma helper0 p h z0 : growing h -> oleq (f z0) (f (evalv a p h z0)).
proof: Proof. elim/um_indf: h z0=>[||k v h IH W /(order_path_min (@trans _)) T] z0 G; rewrite ?eval_undef ?eval0 // evalPtUn //. have K: (k, v) \In pts k v \+ h by apply/InPtUnE=>//; left. have Gh: growing h. - by move=>k1 v1 z1 X1; apply: (G k1); apply/InPtUnE=>//; right. case: ifP=>// P; last by apply: IH. by apply: otrans (IH _ Gh); apply: (G k). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)