fact: Definition consec_list r f := [/\ fgraph f, natp (domain f), sub (range f) (substrate r) & forall i, natp i -> csucc i <c (domain f) -> consecutive r (Vg f i) (Vg f (csucc i))].
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)