proposition: Lemma perm_on_prods c m : c \is a code -> m <= size c -> m <= n -> perm_on [set k : 'I_n | k < m] (\prod_(i <- iota 0 m) 's_[(rev (iota (i - nth 0 c i) (nth 0 c i)))]).
proof: Proof. Proof using. move=> /is_codeP Hc Hmsz Hm. rewrite big_seq; apply big_rec => [| /= i s]; first exact: perm_on1. rewrite mem_iota /= add0n => Him /(perm_onM _); apply => {s}. rewrite big_seq; apply big_rec => [| /= j s]; first exact: perm_on1. rewrite mem_rev mem_iota /= => /andP[_]. move/(_ _ (leq_trans Him Hmsz)): Hc => /subnK -> Hji /(perm_onM _); apply => {s}. have Hj1m := leq_ltn_trans Hji Him. have Hjm := ltn_trans Hji Him. rewrite /perm_on; apply/subsetP => u; rewrite inE unfold_in. apply contraR; rewrite -leqNgt => Hu; apply/eqP/tpermD. - apply/negP => /eqP/(congr1 nat_of_ord). rewrite (inordK (leq_trans Hjm Hm)) => Hju. by have:= leq_trans Hjm Hu; rewrite Hju ltnn. - apply/negP => /eqP/(congr1 nat_of_ord). rewrite (inordK (leq_trans Hj1m Hm)) => Hju. by have:= leq_trans Hj1m Hu; rewrite Hju ltnn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr