proposition: Lemma card_s2f n (s : {set 'I_n}) : #|` s2f s| = #|s|.
proof: Proof. have [m sLm] := ubnP #|s|; elim: m => // m IH s sLm in s sLm *. case: (set_0Vmem s) => [->|[i iIs]]; first by rewrite s2f_set0 cards0. rewrite (cardsD1 i) iIs /= -IH //; last first. by move: sLm; rewrite (cardsD1 i) iIs. rewrite [LHS](cardfsD1 (nat_of_ord i)) (_ : _ \in _); last first. by rewrite mem_s2f. by rewrite s2fD1. Qed.
imports: mathcomp(all_ssreflect finmap)