proposition: Lemma increasingE f m n : increasing f -> m <= n -> f m <= f n.
proof: Proof. move=> fI mLn; rewrite -(subnK mLn). elim: (_ - _) => //= d fL. by apply: leq_trans (fI (d + m)). Qed.
imports: mathcomp(all_ssreflect finmap)