proposition: Lemma fiblist_sub L n (M := restr L n) : fib_listA L -> natp n -> domain L = csucc n -> [/\ fib_listA M, domain M = n & fib_listB L \/ fib_listB M].
proof: Proof. move => [[qa qb qc] qd] nN da. have fgg: fgraph (restr L n) by fprops. have ra: domain M = n by rewrite /M restr_d. have rb: fib_listA M. rewrite /M; split; first saw. move => t/(range_gP fgg); aw => - [i ii]; bw => // ->. apply: qc; apply/(range_gP qa); exists i => //. by rewrite da; apply/(NleP nN); case /(NltP nN): ii. aw; move => i iN iin. move/(NltP nN): (iin) => lin. have ni: inc i n. apply/(NltP nN); exact : (cle_ltT (cleS iN) lin). have rc: inc (csucc i) (domain L) by rewrite da; apply/(NleP nN); case: lin. bw => //;apply: qd => //. split => //. rewrite/ fib_listB ra da (cpred_pr1 (CS_nat nN)). case: (equal_or_not (Vg L n) C0) => rd; first by left; split => //; right. right; split => //; case: (equal_or_not n \0c) => nz; [by left | right]. move: (cpred_pr nN nz) =>[sa sb]. have cnn: inc (cpred n) n by rewrite {2} sb; apply: Nsucc_i. have nd: inc (csucc (cpred n)) (domain L) by rewrite - sb da; apply: Nsucc_i. move: (qd _ sa nd); rewrite - sb; case => //; rewrite /M; bw => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)