proposition: Lemma preimsetD (A B : {set rT}) : f @^-1: (A :\: B) = (f @^-1: A) :\: (f @^-1: B).
proof: Proof. by apply/setP=> y; rewrite !inE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)