proposition: Lemma growE h t1 t2 z0 k v : growing h -> (k, v) \In h -> t1 < k <= t2 -> f (exec a t2 h z0) = f (exec a t1 h z0) -> f (a (exec a k.-1 h z0) v) = f (exec a k.-1 h z0).
proof: Proof. move=>G H /andP [N1 N2] E; have W : valid h by case: H. pose h0 : natmap V := um_filter (le t1) h. pose h1 : natmap V := um_filter [pts x _ | t1 < x <= k.-1] h. pose h2 : natmap V := um_filter [pts x _ | k < x <= t2] h. have subX : forall k m n, k < n -> (m < n) = (m <= n.-1) by move=>?? []. have K1 : k.-1 <= k by rewrite ltnW // (subX t1). have K2 : t1 <= k.-1 by rewrite -(subX t1). have K3 : k.-1 <= k <= t2 by rewrite K1 N2. have K4 : t1 <= k.-1 <= t2 by rewrite K2 (leq_trans K1 N2). have Eh: um_filter (le t2) h = h0 \+ (h1 \+ (k \-> v \+ h2)). - rewrite (umfilt_le_split h N2) (umfilt_le_split h K1). by rewrite (umfilt_le_split h K2) (umfilt_pt_split H) -!joinA. have W1 : valid (h0 \+ (h1 \+ (k \-> v \+ h2))) by rewrite -Eh valid_umfilt. rewrite eval_umfilt (umfilt_le_split h K2) evalUn ?(validAL W1) //; last first. - by move=>??/dom_umfilt[?][/leq_ltn_trans Y] _ /dom_umfilt[?][] /andP [/Y]. rewrite -(eval_umfilt (le t1)); apply: helper2 (validR W1) _ _ _ _ =>//. - by apply: growR W1 _; rewrite -Eh=>k1 v1 z1 /In_umfilt [] _ /G. - by move=>x /dom_umfilt; rewrite (subX t1 x) //; case=>v0 [] /andP []. - by apply/allP=>x /dom_umfilt; case=>v0 [] /andP []. rewrite eval_umfilt Eh evalUn ?(validX W1) -?eval_umfilt // in E. move=>x y /dom_umfilt; case=>v1 [/leq_ltn_trans Y _]. rewrite -(umfilt_pt_split H) -(umfilt_lt_split h K3). by rewrite -(umfilt_lt_split h K4) =>/dom_umfilt; case=>v0 [/andP][/Y]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)