fact: Fixpoint cocode_rec m c (s : 'S_n) : seq nat := if m is m'.+1 then let mo := inord m' in cocode_rec m' (mo - s mo :: c) (s * 's_[iota (s mo) (mo - s mo)]) else c.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr