proposition: Lemma fiblistsAP x: inc x fib_listsA <-> fib_listA 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)