proposition: Lemma card_max_rep_val n m: m.+2 <= n -> card_max_rep n m = 'C(m,n- m.+2).
proof: Proof. move/subnK => {1} <-; set k := _ - _; move: k; elim: {n} m. case; first by rewrite card_max_rep2m. by move => k; rewrite bin0n /= addn2 card_max_repn0. move => n Hr; case; first by rewrite card_max_repn2n bin0. move => k; rewrite 2!addnS card_max_rep_rec ?ltn_paddl //. by rewrite addSnnS Hr - addSn Hr - binS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)