proposition: Lemma braidred_inscode_path c (i : 'I_n) : rev c \is a code -> size c <= n.+1 -> i.+1 < size c -> { p | path braidred ((wcord c) ++ [:: i]) p /\ last ((wcord c) ++ [:: i]) p = wcord (inscode c i) }.
proof: Proof. Proof using. elim: c i => [//= | c0 c IHc] i /= Hcode. have:= Hcode; rewrite rev_cons => /is_code_rconsK {}/IHc Hrec. move/head_revcode : Hcode => Hc0. rewrite !ltnS wcord_cons -catA => Hsz Hisz. case: ltnP => Hi. have:= Hsz; rewrite -ltnS => /ltnW/(Hrec _)/(_ (inord_predS Hi Hisz)){Hrec} /=. rewrite !wcord_cons -cat1s size_inscode cats0. move=> [pth] [Hpath <-]. exists ((wcord c ++ [:: inord i.-1] ++ 'I[c0 .. (size c)]) :: [seq v ++ 'I[c0 .. (size c)] | v <- pth]); split => [| {Hpath}]. - have /= := path_braidred_catl 'I[c0 .. (size c)] Hpath. rewrite -catA /= => ->; rewrite andbT. rewrite /braidred braid_catr // braid_sym. exact: braid_pred_lineC. - rewrite !catA; case: pth => [| p0 p] //=. exact: last_map. case: eqP => [{Hrec}Hi | /eqP Hi1]. case: c0 Hc0 Hi Hisz => [Hc0 | c0 Hc0 Hi Hisz /=]. by rewrite subn0 => ->; rewrite ltnn. rewrite -{1 3}Hi /= subnS prednK ?subn_gt0 //. rewrite rev_cons map_rcons inord_val -!cats1 -catA. exists [:: wcord (c0 :: c)]; split; last by []. rewrite /= andbT; rewrite /braidred; apply/orP; right. apply/reducesP; exists (wcord c ++ 'I[c0 .. (size c)]), i, [::]. rewrite !cats0 -catA; split; first by []. exact: wcord_cons. have {Hi1}Hi : i < size c - c0 by rewrite ltn_neqAle Hi Hi1. case: eqP => [Hi1 | /eqP Hi1]. exists [::]; split; first by []. by rewrite /= wcord_cons rev_cons map_rcons subnS -Hi1 /= inord_val cats1. have {Hi1}Hi : i.+1 < size c - c0 by rewrite ltn_neqAle Hi Hi1. have:= Hsz. rewrite -ltnS => /ltnW/(Hrec _)/(_ (leq_trans Hi (leq_subr _ _))) {Hrec} /=. rewrite wcord_cons size_inscode. move=> [pth] [Hpath <-]. exists ((wcord c ++ [:: i] ++ 'I[c0 .. (size c)]) :: [seq v ++ 'I[c0 .. (size c)] | v <- pth]); split => [| {Hpath}]. - have /= := path_braidred_catl 'I[c0 .. (size c)] Hpath. rewrite -catA /= => ->; rewrite andbT. rewrite /braidred braid_catr // braid_sym. exact: braid_ltn_lineC. - rewrite !catA; case: pth => [| p0 p] //=. exact: last_map. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr