proposition: Lemma fiblist_res4: fib_listsBc \0c = \1c.
proof: Proof. apply /set_of_card_oneP; apply/singletonP; split. exists emptyset; apply:Zo_i; aw; trivial. apply/fiblistsBP; split; last by aw; left. split; last by aw => i _ /in_set0. split; [apply: fgraph_set0 | aw; apply: NS0 | rewrite range_set0; fprops]. move => u v /Zo_P [/fiblistsBP [ [[qa _ _] _] _] qb]. move => /Zo_P [/fiblistsBP [ [[qc _ _] _] _] qd]. by apply: fgraph_exten => //; try ue; rewrite qb => t /in_set0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)