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