proposition: Lemma invset_maxperm : invset (@maxperm n) = Delta.
proof: Proof. apply/setP => /= [[i j]]; rewrite /Delta !inE /= !permE. case: ltnP => //= Hij; apply ltn_sub2l. - exact: (leq_ltn_trans Hij). - by rewrite ltnS. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr