proposition: Lemma fiblist_add_1 L: fib_listB L -> fib_listA (fib_list_plus L C1).
proof: Proof. move => [[ha hb] hc]. have icc: inc C1 C2 by fprops. move: (fiblist_add_x ha icc) => hd; split => //. move: ha =>[qa qb qc]. have nn: ~ inc (domain L) (domain L) by apply: Nat_decent. move => i iN; rewrite domain_setU1; case /setU1_P => h; last first. left; case: hc; rewrite - h; first by move:(@succ_nz i). by rewrite (cpred_pr1 (CS_nat iN)) setU1_V_in // - h; apply: Nsucc_i. 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)