proposition: Lemma card_max_repE n m: card_max_rep n m = \sum_((fib n).-1 <= i < (fib n.+1).-1 | (size (ZeckM i)== m)) 1.
proof: Proof. by rewrite big_mkcond /= /card_max_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)