proposition: Lemma braid_ltn_lineC (i : 'I_n) (sz c : nat) : sz <= n -> i.+1 < sz - c -> c <= sz -> [:: i] ++ 'I[c .. sz] =Br 'I[c .. sz] ++ [:: i].
proof: Proof. Proof using. move=> Hsz Hi Hc0; apply gtn_braidC => u /mapP[ x]. rewrite mem_rev mem_iota => /andP[Hix Hx] ->{u} /=. rewrite subnK // in Hx. rewrite inordK; last by apply (leq_trans Hx). exact: (leq_trans Hi). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr