proposition: Lemma fiblist_add_0 L: fib_listA L -> fib_listB (fib_list_plus L C0).
proof: Proof. move => [ha hb]. have icc: inc C0 C2 by fprops. move: (ha) =>[qa qb qc]. have nn: ~ inc (domain L) (domain L) by apply: Nat_decent. have dd: domain (fib_list_plus L C0) = csucc (domain L). rewrite domain_setU1 succ_of_nat //. move: (fiblist_add_x ha icc) => hc; split => //; last first. right; rewrite dd (cpred_pr1 (CS_nat qb)) setU1_V_out //. split => // i iN; rewrite domain_setU1; case /setU1_P; last first. by move ->; right;rewrite setU1_V_out. move => h. have idl: inc i (domain L). by apply/(NltP qb); apply /(cleSltP iN); move/(NltP qb): h; case. by rewrite ! setU1_V_in //; apply: hb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)