fact: Definition strict_decreasing_fun f r r' := [/\ order r, order r', function_prop f (substrate r) (substrate r') & forall x y, glt r x y -> glt r' (Vf f y) (Vf f x)].
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)