proposition: Lemma morphpre_proper R S : R \subset f @* D -> S \subset f @* D -> (f @*^-1 R \proper f @*^-1 S) = (R \proper S).
proof: Proof. by move=> dQ dR; rewrite /proper !morphpreSK. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)