proposition: Lemma growIn h t1 t2 z0 : growing a f h -> t1 <= t2 -> f (exec a t1 h z0) <= f (exec a t2 h z0).
proof: Proof. by move=>G N; move: (growI z0 G N); rewrite leq_eqVlt /oleq/ord orbC. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)