proposition: Lemma Zeckv_bound3 l n: uniq l -> (all (leq^~ n) l) -> (Zeck_val l).+2 <= fib n.+4.
proof: Proof. move /sorted_gtn;set l' := (rev (sort leq l)) => sa /allP sb. have hc: perm_eq l l'. rewrite /l' perm_sym; apply:(@perm_trans _ (sort leq l)). by elim:(sort leq l)=> // a s h; rewrite rev_cons perm_rcons perm_cons. by apply/permPl; apply: perm_sort. have ->: (Zeck_val l) = (Zeck_val l') by apply: perm_big. have:(all (leq^~ n) l'). apply/allP => x; rewrite -(perm_mem hc x); apply: sb. move: sa; case l'. by move => _ _; rewrite Zeckv_nil -[1]/(fib 2) //; apply:fib_smonotone_bis. move => a s pa pb; apply: (leq_trans (Zeckv_bound0 pa)). by apply: fib_monotone; rewrite !ltnS; apply/(allP pb); rewrite inE eqxx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)