fact: Definition closure f r := [/\ increasing_fun f r r, (forall x, inc x (substrate r) -> gle r x (Vf f x)) & (forall x, inc x (substrate r) -> Vf f (Vf f x) = Vf f x)].
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)