proposition: Lemma size_all_leq n t : (forall i, i < n -> i \in t) -> n <= size t.
proof: Proof. move=> H. pose s := undup (filter (gtn n) t). have Hperm : perm_eq s (iota 0 n). apply: (uniq_perm (undup_uniq _) (iota_uniq _ _)). move=> i; rewrite /s mem_undup mem_iota /= add0n mem_filter /=. apply/idP/idP => [/andP[->] //| Hi]. by rewrite Hi (H i Hi). have <- := size_iota 0 n. rewrite -(perm_size Hperm) /s. apply: (leq_trans (size_undup _)). by rewrite size_filter; apply: count_size. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp