proposition: Lemma ZeckM_bound2 n a: (fib a.+3).-1 <= n < (fib a.+4).-1 -> a = head 0 (ZeckM n).
proof: Proof. case: (posnP n) => np; first by rewrite np fib_ge2_alt. rewrite -ltnS -(ltnS n.+1) -!fib_pos => la. move:(ZeckM_bound1 np); rewrite -ltnS -(ltnS n.+1) -!fib_pos => lb. by move /eqP:(fib_partition la lb); rewrite !eqSS => /eqP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)