proposition: Lemma imset_inj : injective (fun s : {set T1} => imset f (mem s)).
proof: Proof. move=> s1 s2 /eqP; rewrite eqEsubset => /andP[H12 H21]. move: f_inj => /subset_imsetK Hinj. apply/eqP; rewrite eqEsubset. by rewrite (Hinj _ _ H12) (Hinj _ _ H21). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)