proposition: Lemma consec_pow_pr0 r f x: inc f (consec_lists_for r x) <-> (consec_list_for r f x).
proof: Proof. split; first by move/Zo_hi. move => h; apply:Zo_i => //. move:h =>[[ha hb hc hd] _]; apply/fgraphsP; split => //. by move: (NS_inc_nat hb). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)