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