proposition: Lemma ZeckM_rec1 n a: (fib a.+3).-1 <= n < (fib a.+4).-1 -> ZeckM (n + (fib a.+3)) = a.+1::ZeckM n.
proof: Proof. move /ZeckM_bound2 => sa. move/andP: (ZeckM_prop2 n) => [ss /eqP nv]. apply:ZeckM_prop3; rewrite/max_rep Zeckv_cons nv addnC eqxx. by rewrite spec_sorted_rec ss sa; case:(ZeckM n) => // nb l /=; rewrite eqxx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)