proposition: Lemma card_max_repn0 n: card_max_rep n.+3 0 = 0.
proof: Proof. rewrite card_max_repE big_hasC => //; apply /hasPn => i. rewrite mem_index_iota size_eq0 => fb; apply /eqP => ln. move: (ZeckM_prop2 i); rewrite /max_rep ln Zeckv_nil => /andP[_ /eqP iz]. by move: fb; rewrite - iz leqn0 (fib_ge2_alt). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)