proposition: Lemma reducesP (u v : seq 'I_n) : reflect (exists x i y, u = x ++ [:: i; i] ++ y /\ v = x ++ y) (reduces u v).
proof: Proof. Proof using. elim: u v => [| a u IHu] v. apply (iffP idP) => /=; first by case v. by move=> [x] [i] [y] []; case x. case: u IHu => [| b l] IHu. apply (iffP idP) => /=; first by case v. by move=> [x] [i] [y] []; case: x => [| x0 [|x1 x]]. case: v => [| v0 v] /=. rewrite orbF; apply (iffP idP). - move=> /andP[/eqP Ha /eqP Hl]; subst a l. by exists [::], b, [::]. - move=> [x] [i] [y] []; case: x => [| x0 x] //. by case: y => //= [] [-> -> ->]; rewrite eq_refl. apply (iffP idP). - move=> /orP[] /andP[/eqP ->{a}]. + move=> /eqP Hl; subst l. by exists [::], b, (v0 :: v). + move/IHu => {IHu} [x] [i] [y] [Hbl ->{v}]. by exists (v0 :: x), i, y => /=; rewrite Hbl. - move=> [x] [i] [y] []; case: x => [| x0 x] /=. + by move=> [-> -> ->] <-; rewrite !eq_refl. + move=> [Ha H1] [H0 H2]; subst a v0. apply/orP; right; rewrite eq_refl /=. by apply/IHu; exists x, i, y. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr