proposition: Lemma morphim_idm A B : B \subset A -> idm A @* B = B.
proof: Proof. rewrite /morphim /= /idm => /setIidPr->. by apply/setP=> x; apply/imsetP/idP=> [[y By ->]|Bx]; last exists x. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)