proposition: Lemma morphpreIdom R : D :&: f @*^-1 R = f @*^-1 R.
proof: Proof. by rewrite /morphim setIA setIid. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)