proposition: Lemma Zeck_split a l x: sorted llen (a :: l) -> x <= fib a.+2 -> Zeckp (x + (Zeck_val l)) = Zeckp x + Zeckp (Zeck_val l).
proof: Proof. move => sr le1; move:(uniq_llen sr) (path_all_llen sr) => h sa. rewrite (Zeckp_prop1 h) {2}/Zeckp - {1}(Zeck_zeck_val x) /Zeck_val /Zeck_valp. rewrite - !big_cat /=; apply: Zeckp_prop1; rewrite cat_uniq h Zeck_uniq /=. rewrite andbT; apply/negP => /hasP [t /(allP sa)] => /= /ltnW sb tz. move:(leq_trans (allP (Zeck_val_bounded x) _ tz) le1). by rewrite leqNgt (fib_smonotone_bis sb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)