proposition: Lemma fiblistsBP x: inc x fib_listsB <-> fib_listB x.
proof: Proof. split; first by move/Zo_hi. move => h; apply: Zo_i => //; apply/ fgraphsP. by move: h => [[[qa qb qc] _] _]; split => // t; apply: NS_inc_nat. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)