proposition: Lemma card_min_rep_valbis n m: 0< m< n -> card_min_rep n m = 'C(n-m-1,m.-1).
proof: Proof. move => /andP[sa sb]; rewrite -subnDA -{1}(subnK sb) addn1 -{2 3} (prednK sa). by rewrite card_min_rep_val. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)