proposition: Lemma eq_preimset f g R : f =1 g -> f @^-1: R = g @^-1: R.
proof: Proof. by move=> eqfg; apply/setP => y; rewrite !inE eqfg. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)