proposition: Lemma braid_pred_lineC (i : 'I_n) (sz c : nat) : sz <= n -> i < sz -> c <= sz -> sz - c < i -> ([:: inord i.-1] ++ 'I[c .. sz]) =Br ('I[c .. sz] ++ [:: i]).
proof: Proof. Proof using. rewrite /= cats1 => Hsz Hisz Hc0 Hi. rewrite (iota_cut_i Hc0 Hi Hisz) !rev_cat !map_cat -cats1 -!catA. set A := map _ _; rewrite {1 3}/rev [map _ _]/= inord_val; set B := map _ _. apply (braid_trans (y := A ++ [:: i; inord i.-1] ++ (i :: B))); first last. do 2 apply braid_catr; rewrite -cat1s; apply ltn_braidC => u. rewrite {}/B {A} => /mapP[x]. rewrite mem_rev mem_iota => /andP[_]. case: i Hisz Hi (inord_predS Hi Hisz) => [[| i] Hi] //= Hisz. rewrite !ltnS => /subnKC -> Hszi Hx ->. by rewrite inordK //; apply (ltn_trans Hx); apply ltnW. rewrite -[i :: B]cat1s -cat1s !catA; apply: braid_catl => {B}. apply (braid_trans (y := A ++ [:: inord i.-1; i; inord i.-1])); first last. rewrite -catA /=; apply braid_catr; apply rule_gencongr => /=. rewrite eq_refl /=. suff -> : (inord (n' := n0) i.-1).+1 = i by rewrite eq_refl /= mem_seq1 eq_refl. rewrite inordK; last by apply (leq_ltn_trans (leq_pred _)). by rewrite (ltn_predK Hi). rewrite -[inord i.-1 :: i :: _]cat1s catA; apply braid_catl. rewrite /A; case: (ltnP i sz) => Hi'. apply gtn_braidC => u. rewrite {}/A => /mapP[x]. rewrite mem_rev mem_iota => /andP[Hix Hx] ->{u} /=. rewrite subnKC // in Hx. rewrite inordK; last by apply (leq_ltn_trans (leq_pred _)). rewrite (ltn_predK Hi). by rewrite inordK; last apply: (leq_trans Hx). move: Hi'; rewrite -ltnS => /ltnW. by rewrite /leq => /eqP ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr