proposition: Theorem invset_inj : injective invset.
proof: Proof. exact: (can_inj invsetK). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr