proposition: Lemma perm_on_cocode_recP m c s0 s : m <= n -> is_partcode m c -> s0 = s * 's_[word_of_partcocode m c] -> perm_on [set k : 'I_n | k < m] s -> let cf := cocode_rec m c s in cf \is a code /\ s0 = 's_[wordcd cf].
proof: Proof. Proof using. move=> Hm Hcode -> {s0}. elim: m => [| m IHm] in c s Hm Hcode * => Hon /=. split; first by apply/is_codeP => i; rewrite -{3}(addn0 i); apply Hcode. suff -> : s = 1 by rewrite mul1g. apply permP => i; rewrite perm1. by apply: (out_perm Hon); rewrite inE. pose mo := Ordinal Hm. have -> : inord m = mo by apply val_inj; rewrite /= inordK. have : mo \in [set k : 'I_n | k < m.+1] by rewrite inE. rewrite -(perm_closed _ Hon) inE ltnS => Hsm. move/(_ _ _ (ltnW Hm)): IHm => Hrec. have {Hcode}/Hrec Hrec: is_partcode m (mo - s mo :: c). rewrite /is_partcode {Hrec} => [[_ | i]] /=. by rewrite add0n; exact: leq_subr. by rewrite ltnS addSnnS => /Hcode. set srec := s * _. have {}/Hrec /= : perm_on [set k : 'I_n | k < m] srec. rewrite {Hrec} /srec /perm_on; apply/subsetP => k. rewrite !inE; apply contraR; rewrite -ltnNge permM ltnS => Hmk. apply/eqP; case (leqP k m) => Hkm. + have -> : k = mo by apply val_inj; apply/eqP; rewrite /= eqn_leq Hmk Hkm. exact: cycleij_j. + have -> : s k = k by apply (out_perm Hon); rewrite inE -ltnNge. rewrite cycleij_gt // -ltnNge. move=> [Hcode <-]; split; first exact: Hcode. rewrite {Hcode}/srec -mulgA; congr (s * _). rewrite /word_of_partcocode /= addn0 (subKn Hsm) big_cat /=. rewrite mulgA prodsK mul1g; apply congr_big => //; congr flatten. rewrite -(addn0 1%N) iotaDl -map_comp. by apply eq_map => i /=; rewrite addnA addn1. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr