proposition: Lemma drop_take_iota a b c : a <= b <= c -> drop a (take b (iota 0 c)) = [seq n <- iota 0 c | a <= n < b].
proof: Proof. move=> /andP[ab bc]. set f := fun n => a <= n < b. rewrite -(subnKC bc) iotaD take_cat size_iota subnn take0 add0n (ltnn b) cats0 filter_cat. rewrite (_ : filter f (iota b (c-b)) = [::]) ; last first. apply/eqP/negPn ; rewrite -has_filter ; apply/hasPn => l. rewrite mem_iota (subnKC bc) /f negb_and => /andP [bl _]. by rewrite -leqNgt bl orbT. rewrite cats0 -(subnKC ab) iotaD drop_cat size_iota subnn drop0 add0n (ltnn a) filter_cat. rewrite (_ : filter f (iota 0 a) = [::]) ; last first. apply/eqP/negPn ; rewrite -has_filter ; apply/hasPn => l. rewrite mem_iota /f negb_and add0n => /andP [_ H]. by rewrite -ltnNge H orTb. rewrite cat0s. apply/esym/all_filterP/allP => l. by rewrite mem_iota /f (subnKC ab). Qed.
imports: mathcomp(all_ssreflect fingroup perm)