proposition: Lemma std_rconsK (u : seq S) (v : seq T) a b : std (rcons u a) = std (rcons v b) -> std u = std v.
proof: Proof. move/eqP/std_eq_invP/eq_invP => [/eqP]; rewrite !size_rcons eqSS => /eqP Hsz Hinv. apply/eqP/std_eq_invP/eq_invP; split; first exact Hsz. move=> i j /andP[Hij Hj]. have {}/Hinv : i <= j < (size u).+1 by rewrite Hij /=; exact: (leq_trans Hj). by rewrite !nth_rcons -Hsz (leq_ltn_trans Hij Hj) Hj. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordtype permcomp