proposition: Lemma fiblist_add_x L x: fib_list L -> inc x C2 -> fib_list (fib_list_plus L x).
proof: Proof. move => [qa qb qc] xd. have nn: ~ inc (domain L) (domain L) by apply: Nat_decent. have dd: domain (fib_list_plus L x) = csucc (domain L). rewrite domain_setU1 succ_of_nat //. have ff: fgraph (fib_list_plus L x) by apply: fgraph_setU1. split. + done. + by rewrite dd; apply: NS_succ. + move => t /(range_gP ff); rewrite domain_setU1 => - [u ua ->]. case/setU1_P: ua => ua. rewrite setU1_V_in //; apply: qc; apply/(range_gP qa); ex_tac. by rewrite ua setU1_V_out. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)