proposition: Lemma card_max_rep_smalln n m: n < m.+2 -> card_max_rep n m = 0.
proof: Proof. case:n => [|[| [|n]]]; rewrite ? card_max_rep0m ? card_max_rep1m // ! ltnS. by move/gtn_eqF; rewrite card_max_rep2m => ->. move => lnm; rewrite card_max_repE big_hasC => //; apply /hasPn => x. rewrite mem_index_iota => ltn; apply/eqP => eq1. by move:(leq_ltn_trans (ZeckM_bound3 ltn) lnm); rewrite eq1 ltnn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)