proposition: Lemma eq_inv_rconsK (a : S) u (b : T) v : eq_inv (rcons u a) (rcons v b) -> eq_inv u v.
proof: Proof. rewrite -!eq_invP !size_rcons => [][Hsz H]. move: Hsz => /eqP; rewrite eqSS => /eqP Hsz; rewrite Hsz; rewrite Hsz in H. split => // i j /andP[Hi Hj]. have {}/H : i <= j < (size v).+1. by rewrite Hi /=; exact: (ltn_trans Hj). by rewrite !nth_rcons Hsz Hj (leq_ltn_trans Hi Hj). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp