proposition: Lemma FR_split n (p := fib (Zeck_li n).+2) (m := n - p): n != 0 -> n = p + m /\ (m = 0 \/ llen (Zeck_li n) (Zeck_li m)).
proof: Proof. rewrite /m/p; clear p m. case:n => // n _; move: (Zeck_prop1 (n:=n.+1) isT) => [a [l [pa pb pc]]]. rewrite /Zeck_li pb rev_cons last_rcons pc Zeckv_cons addKn; split => //. move: pa;case l; first by left;rewrite Zeckv_nil. move => u v /= /andP [sa sb]; right. by rewrite /Zeck_val - sum_rev ZeckP ? rev_sorted //= rev_cons last_rcons. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)