fact: Definition normal_ofs1 (f: fterm) u:= sincr_ofsu f u /\ (forall X, (forall x, inc x X -> u <=o x) -> nonempty X -> \osup (fun_image X f) = f (\osup X)).
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)