proposition: Lemma sincr_incr f: sincr_ofs f -> (forall a b, a <=o b -> f a <=o f b).
proof: Proof. move => h x y xy. case:(ole_eqVlt xy) => exy; last by exact: (proj1 (h _ _ exy)). rewrite - exy; exact (oleR (proj31_1 (h _ _ (oltS (proj31 xy))))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)