proposition: Lemma card_max_rep41: card_max_rep 4 1 = 1.
proof: Proof. by rewrite /card_max_rep big_ltn// big_ltn// big_geq//= ZeckM2 (ZeckM_fibm2 2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)