proposition: Lemma Zeck_zeck_val n: Zeck_val (Zeck n) = n.
proof: Proof. elim: n {-2} n (leqnn n). by move => n; rewrite leqn0 => /eqP ->; rewrite Zeck_0 Zeckv_nil. move=> n IH n1; rewrite leq_eqVlt; case/orP=> [/eqP ->|Hn]; last first. by apply: IH; rewrite -ltnS. rewrite Zeck_S' Zeckv_cons; move:(fib_content_large n) => h. by rewrite (IH _ h); apply: subnKC; move/andP: (fib_contentP n) => []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)