proposition: Lemma disjoint_imset (A B : {set T1}) : [disjoint A & B] -> [disjoint [set f x | x in A] & [set f x | x in B]].
proof: Proof. rewrite -!setI_eq0 => /eqP Hdisj. rewrite -imsetI; last by move=> x y _ _; exact: f_inj. by rewrite imset_eq0 Hdisj. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)