proposition: Lemma imset_disjoint (A B : {pred T}) : [disjoint f @: A & f @: B] = [disjoint A & B].
proof: Proof. apply/pred0Pn/pred0Pn => /= [[? /andP[/imsetP[x xA ->]] xB]|]. by exists x; rewrite xA -(mem_imset (mem B) x inj_f). by move => [x /andP[xA xB]]; exists (f x); rewrite !mem_imset ?xA. Qed.
imports: mathcomp(all_ssreflect)