proposition: Lemma invsetP s : is_invset (invset s).
proof: Proof. split; first exact: invset_Delta. - rewrite /=/invset => j i k /=; rewrite !inE /=. by move=> /andP[/ltn_trans iltj /(ltn_trans _) siltsj] /andP[/iltj-> /siltsj->]. - rewrite /=/invset => j i k /=; rewrite !inE /=. have logic A B : ((~~ (A && B)) && A) = (A && ~~ B) by case: A; case: B. rewrite !{}logic -!leqNgt. by move=> /andP[/ltn_trans iltj /leq_trans siltsj] /andP[/iltj-> /siltsj->]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr