proposition: Lemma preimsetC (A : {set rT}) : f @^-1: (~: A) = ~: f @^-1: A.
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)