proposition: Lemma growI h t1 t2 z0 : growing h -> t1 <= t2 -> oleq (f (exec a t1 h z0)) (f (exec a t2 h z0)).
proof: Proof. move=>G N; case W: (valid h); last first. - by move/negbT/invalidE: W=>->; rewrite !eval_undef. rewrite eval_umfilt [in X in oleq _ X]eval_umfilt (umfilt_le_split h N). rewrite evalUn; first by apply: helper0=>x y z /In_umfilt [_ /G]. - by rewrite -(umfilt_le_split h N) valid_umfilt. by move=>??/dom_umfilt[?][/leq_ltn_trans Y _]/dom_umfilt[?][/andP[/Y]]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)