proposition: Lemma perm_onto s : codom s =i predT.
proof: Proof. by apply/subset_cardP; rewrite ?card_codom ?subset_predT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)