proposition: Lemma expansion_bounded1 f k b : expansion f b k -> inc f (sub_fgraphs Nat b).
proof: Proof. move => [bN kn _ [pd pe pf]]. apply /sub_fgraphsP; exists k; first by move => t; apply:(NS_inc_nat kn). apply/gfunctions_P2; split => // t/(range_gP pd) [x /pf xdf ->]. apply /(oltP (OS_nat bN)); exact:(oclt xdf). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)