proposition: Lemma preimset_proper (A B : {set rT}) : B \subset codom f -> A \proper B -> (f @^-1: A) \proper (f @^-1: B).
proof: Proof. move=> sBc /properP[sAB [u Bu nAu]]; rewrite properE preimsetS //=. by apply/subsetPn; exists (iinv (subsetP sBc _ Bu)); rewrite inE /= f_iinv. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)