proposition: Lemma fiblist_res2 n: natp n -> fib_listsAc (csucc n) = fib_listsAc n +c fib_listsBc n.
proof: Proof. rewrite /fib_listsAc /fib_listsBc. set A := Zo _ _; set B := Zo _ _ ; set C := Zo _ _ => nN. set B' := Zo fib_listsB (fun z => domain z = csucc n). set C' := A -s B'. have di1: disjoint B' C' by apply: set_I2Cr. have ->: A = B' \cup C'. rewrite setU2_Cr // => t /Zo_P [/fiblistsBP /proj1 qa qb]. by apply:Zo_i => //; apply /fiblistsAP. rewrite (csum2_pr5 di1) - csum2cr - csum2cl; apply: f_equal2. symmetry; exact:(fiblist_res1 nN). symmetry; apply/card_eqP. exists (Lf (fun z => fib_list_plus z C1) C C'). hnf; saw; apply: lf_bijective. + move => z /Zo_P [/fiblistsBP qa qb]. move: (fiblist_add_1 qa); set r := (fib_list_plus z C1) => ra. have dr: domain r = csucc n by rewrite domain_setU1 qb succ_of_nat. apply /setC_P; split; first by apply: Zo_i => //; apply/fiblistsAP. move/Zo_P /proj1/fiblistsBP/proj2; case. rewrite dr; apply: succ_nz. rewrite dr (cpred_pr1 (CS_nat nN)); rewrite /r /fib_list_plus qb. move: qa => [[[sa sb sc] _] _ ]. by rewrite setU1_V_out; fprops; rewrite qb; apply: Nat_decent. + move => u v /Zo_P [/fiblistsBP qa qb] /Zo_P [/fiblistsBP 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 /setC_P [ /Zo_P [/fiblistsAP qa qb] /Zo_P qc1]. have nBy: ~ fib_listB y. by move => b; case: qc1; split => //; apply/fiblistsBP. case: (equal_or_not (Vg y n) C0) => qf. case: nBy; split => //. by right; rewrite qb (cpred_pr1 (CS_nat nN)). move: (fiblist_sub qa nN qb) =>[qc qd]; case => // qe. have ndy: inc n (domain y) by rewrite qb; apply: Nsucc_i. case : (fiblist_p1 (proj1 qa) ndy ) => //vn0. exists (restr y n); first by apply: Zo_i => //; apply/fiblistsBP. move: qa => [[ra rb rc] _]. have aux: ~ inc n n by apply: Nat_decent. have aux2: fgraph (restr y n) by fprops. apply: fgraph_exten => //. - by apply: fgraph_setU1; aw. - 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 /fib_list_plus h; aw; rewrite setU1_V_out; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)