proposition: Lemma eval_le_ind A R a (P : R -> Prop) (h : natmap A) t1 t2 (z0 : R) : t1 <= t2 -> P (eval a (le t1) h z0) -> (forall k v z0, (k, v) \In h -> t1 < k <= t2 -> P z0 -> P (a z0 k v)) -> P (eval a (le t2) h z0).
proof: Proof. by move=>T P0 H; rewrite (eval_le_split a h z0 T); apply: eval_ind. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)