proposition: Lemma set_predleq_size r k l : k + l <= r -> #|[set i : 'I_r | nat_of_ord i \in iota k l]| = l.
proof: Proof. elim: l => [kr | l IH HSl]. - apply/eqP; rewrite cards_eq0; apply/eqP. apply/setP => i; by rewrite !inE. - rewrite addnS in HSl. have : k + l <= r by apply: (leq_trans _ HSl); apply leqnSn. move/IH => Hl. rewrite -sum1_card (bigD1 (Ordinal HSl)) /=. rewrite (_ : \sum_(i in [set i0 : 'I_r | nat_of_ord i0 \in iota k l.+1] | _) 1 = \sum_(i in [set i0 : 'I_r | nat_of_ord i0 \in iota k l]) 1); last first. apply eq_bigl => i; rewrite !in_set. case/boolP : (i != Ordinal HSl) => Hcase. - rewrite andbT -addn1 iotaD /= mem_cat !inE. set tmp := _ == _ + _. suff -> : tmp = false by rewrite orbC. apply/eqP/eqP. move: Hcase; apply: contra => /eqP Hcase. by apply/eqP; apply val_inj. - rewrite negbK in Hcase. move/eqP : Hcase => ->. by rewrite andbC /= mem_iota /= ltnn andbC. by rewrite sum1_card Hl add1n. rewrite in_set in_cons mem_iota /=. destruct l; first by rewrite addn0; apply/orP; left. apply/orP; right. apply/andP; split; by [rewrite addnS ltnS leq_addr | rewrite ltn_add2r]. Qed.
imports: mathcomp(all_ssreflect fingroup perm zmodp ssralg) ssr_ext f2