proposition: Lemma injmD1 A : f @* A^# = (f @* A)^#.
proof: Proof. by have:= morphimDG A injf; rewrite morphim1. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)