proposition: Lemma size_invseq s t : invseq s t -> size s = size t.
proof: Proof. rewrite /invseq => /andP[Hst Hts]. by apply/eqP; rewrite eqn_leq !size_leq_invseq. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp