proposition: Lemma card_min_rep_val n m : card_min_rep (n+m.+2) m.+1 = 'C(n,m).
proof: Proof. elim:n m. case; first by rewrite card_min_repn1. by move => m; rewrite bin0n card_min_rep_rec !card_min_rep_small /=. move => n H; case; first by rewrite bin0; rewrite card_min_repn1 addn2 //. by move => m; rewrite 2!addnS card_min_rep_rec addSnnS -addnS H H binS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)