proposition: Lemma invset_maxpermMl s : invset (maxperm * s) = Delta :\: [set (maxperm p.2, maxperm p.1) | p in invset s].
proof: Proof. rewrite /invset -setP => /=[[i j]]; rewrite !inE /= [RHS]andbC. case: ltnP => //= iltj; rewrite !permM. apply/idP/idP => [Hsm|]. - apply/imsetP => /=[] [[k l]]. rewrite inE /= => /andP[kltl slltsk] [Hi Hj]; subst i; subst j. move: Hsm; rewrite !maxpermK => /(ltn_trans slltsk). by rewrite ltnn. - move/imsetP => /= H; rewrite ltnNge; apply/negP. rewrite leq_eqVlt val_eqE !(inj_eq perm_inj). rewrite -[i == j]val_eqE (ltn_eqF iltj) /= => Hsm. apply: H; exists (maxperm j, maxperm i); rewrite ?inE /= ?maxpermK //. rewrite {}Hsm andbT !permE /=. apply ltn_sub2l => //. exact: (leq_ltn_trans iltj). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr