proposition: Lemma card_min_rep_small n m: 0 < n <= m -> card_min_rep n m = 0.
proof: Proof. case: n => [| [| n /= lnm]] //; first by rewrite card_min_rep1m. rewrite card_min_repE big_hasC => //; apply /hasPn => i. rewrite mem_index_iota => eqa. move: (sorted_ggenW (Zeck_ggen i)); rewrite (Zeck_S eqa) => /size_sorted /=. set s := size _ => ls. have lsn: s.+2 <= n.+2 by rewrite !ltnS; apply:ls. by rewrite (ltn_eqF (leq_trans lsn lnm)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)