proposition: Lemma normal_function_incr f a b: ordinalp a -> ordinalp b -> normal_function f a b -> (forall u v, u <=o v -> v <o a -> Vf f u <=o Vf f v).
proof: Proof. move => oa ob [[ff sf tf] pa pb] u v uv va. have ua:=(ole_ltT uv va). have iua: inc u a by apply/(oltP oa). have iva: inc v a by apply/(oltP oa). case:(ole_eqVlt uv)=> nuv; last by case:(pa _ _ iua iva nuv). have /(Os_ordinal ob) /oleR ov : inc (Vf f v) b by Wtac. by rewrite nuv. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)