fact: Definition factm of 'ker q \subset 'ker f & G \subset H := fun x => f (repr (q @*^-1 [set x])).
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)