proposition: Lemma ZeckM_bound1 n (a := head 0 (ZeckM n)): 0 < n -> (fib a.+3).-1 <= n < (fib a.+4).-1.
proof: Proof. rewrite /a; move/andP:(ZeckM_prop2 n) => [ h /eqP {1 3 4} <-]. by move: h;case: (ZeckM n) => [| b l / max_rep_bound //]; rewrite Zeckv_nil. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)