proposition: Lemma Zeck_fib n: Zeck (fib n.+2) = [:: n].
proof: Proof. have eq1:= (fib_pos n.+1). by rewrite eq1 Zeck_S' fib_content_eq - eq1 subnn Zeck_0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)