proposition: Lemma fiblist_p1 L x: fib_list L -> inc x (domain L) -> Vg L x = C0 \/ Vg L x = C1.
proof: Proof. move =>[qa qb qc] xdl. have vr : inc (Vg L x) (range L) by apply/(range_gP qa); ex_tac. by move:(qc _ vr) => /set2_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)