proposition: Lemma iota_cut_i (l b : nat) (i : 'I_n) : l <= b -> b - l < i -> i < b -> iota (b - l) l = (iota (b - l) (i.-1 - (b - l))) ++ [:: i.-1; i : nat] ++ (iota i.+1 (b - i.+1)).
proof: Proof. Proof using. move=> Hbl Hi1 Hi2. have Hbli : b - l <= i.-1 by rewrite -ltnS (ltn_predK Hi1). have -> : [:: i.-1; i : nat] = iota i.-1 2 by rewrite /= (ltn_predK Hi1). rewrite -{2}(subnKC Hbli) catA -iotaD. rewrite -addSnnS addn1 -subSn // (ltn_predK Hi1) -subSn; last by apply ltnW. have Hbli1 := leq_trans (ltnW Hi1) (leqnSn _). rewrite -{2}(subnKC Hbli1) -iotaD addnC (addnBA _ Hbli1). by rewrite (subnK Hi2) (subKn Hbl). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr