proposition: Lemma ltn_braidC (s : seq 'I_n) (i : 'I_n) : (forall u, u \in s -> u.+1 < i) -> [:: i] ++ s =Br s ++ [:: i].
proof: Proof. Proof using. rewrite cat1s cats1. move=> Hs; elim: s => [| s0 s IHs] //= in Hs *. apply (braid_trans (y := [:: s0, i & s])). - rewrite -[[:: i, s0 & s]]/([:: i; s0] ++ s) -[[:: s0, i & s]]/([:: s0; i] ++ s). apply braid_catl; apply rule_gencongr => /=. have /Hs -> : s0 \in s0 :: s by rewrite inE eq_refl. by rewrite orbT mem_seq1 eq_refl. rewrite -[s0 :: _]cat1s -[s0 :: rcons _ _]cat1s. by apply braid_catr; apply IHs => u Hu; apply Hs; rewrite inE Hu orbT. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr