fact: Definition decreasing_strict_sequence f r := [/\ fgraph f, domain f = Nat, sub (range f) (substrate r) & forall n m, natp n -> natp m -> n <c m -> glt r (Vg f m) (Vg f n)].
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)