proposition: Lemma invset_maxpermMr s : invset (s * maxperm) = Delta :\: invset s.
proof: Proof. rewrite /invset -setP => /= [[i j]]. rewrite /Delta !inE /= !permM ![maxperm _]permE. case: (ltnP i j) => //= iltj; rewrite andbT -leqNgt. rewrite [RHS]leq_eqVlt val_eqE (inj_eq perm_inj). rewrite -[i == j]val_eqE (ltn_eqF iltj) /=. apply/idP/idP => [| siltsj]. - apply contraLR; rewrite -!leqNgt => H. by apply leq_sub2l; rewrite ltnS. - apply ltn_sub2l => //. exact: (leq_ltn_trans siltsj). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr