proposition: Lemma card_min_repE n m: card_min_rep n m = \sum_((fib n) <= i < (fib n.+1)| (size (Zeck i)== m)) 1.
proof: Proof. by rewrite big_mkcond /= /card_min_rep; apply: eq_big. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)