proposition: Lemma ZeckM_bound3 n a: (fib a.+3).-1 <= n < (fib a.+4).-1 -> size (ZeckM n) <= a.+1 ?= iff (n== (fib (a.+4)).-2).
proof: Proof. move => h. move:(ZeckM_bound2 h); move: (ZeckM_prop2 n) h => /andP[];case: (ZeckM n). by rewrite Zeckv_nil => _ /eqP <-; rewrite fib_ge2_alt /=. move => b l ss zv _ /= ->; apply/leqifP. move:(ZeckM_prop2 (fib b.+4).-2) => /andP[wa /eqP zz]. case: eqP => nv. have ea: Zeck_val (b :: l) = Zeck_val (ZeckM (fib b.+4).-2). by rewrite zz -nv (eqP zv). rewrite -/(size (b::l)) (max_rep_unique ss wa ea) ZeckM_fibm2. by rewrite size_rev size_iota. move /leqifP: (size_sorted (spec_sorted_sorted ss)); rewrite ltnS. case: eqP => // lv; move: zv; rewrite lv -rev_rcons -iota_Sr - ZeckM_fibm2 zz. by move => h;case: nv; rewrite (eqP h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)