proposition: Lemma fiblist_res1 n: natp n -> fib_listsAc n = fib_listsBc (csucc n).
proof: Proof. move => nN; apply/card_eqP. set E := Zo _ _ ; set F := Zo _ _. exists (Lf (fun z => fib_list_plus z C0) E F). hnf; saw; apply: lf_bijective. + move => z /Zo_P [/fiblistsAP qa qb]; apply: Zo_i. by apply/fiblistsBP; apply: fiblist_add_0. rewrite domain_setU1 qb succ_of_nat //. + move => u v /Zo_P [/fiblistsAP qa qb] /Zo_P [/fiblistsAP qc qd] sv. move: qa qc => [[ra rb rc] _] [[rd re rf] _]. apply: fgraph_exten => //; first by rewrite qb qd. have nn: ~ inc (domain u) (domain u) by apply: Nat_decent. have nn': ~ inc (domain v) (domain v) by apply: Nat_decent. move => i idu. move: (f_equal (Vg ^~i) sv); rewrite setU1_V_in // setU1_V_in //. by rewrite qd - qb. - move => y /Zo_P [/fiblistsBP qa qb]. move: (fiblist_sub (proj1 qa) nN qb) =>[qc qd _]. exists (restr y n); first by apply: Zo_i => //; apply/fiblistsAP. move: qa => [[[ra rb rc] _]]. rewrite /fib_list_plus; aw; rewrite qb (cpred_pr1 (CS_nat nN)); case. by move: (@succ_nz n). move => vn0. have aux: ~ inc n (domain (restr y n)). aw. by apply: Nat_decent. have aux2: fgraph (restr y n) by fprops. apply: fgraph_exten => //. - by apply: fgraph_setU1. - by rewrite domain_setU1; aw; rewrite qb succ_of_nat. - rewrite qb (succ_of_nat nN) => t /setU1_P; case => h. by rewrite setU1_V_in //; bw => //; aw. by rewrite h setU1_V_out. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)