proposition: Lemma cast_lshift j : cast_ord (esym (addn0 n)) j = lshift 0 j.
proof: Proof. by apply val_inj. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg fingroup morphism perm gproduct) mathcomp(ssrnum matrix vector mxalgebra algC) mathcomp(classfun character mxrepresentation) tools ordcast partition sorted permcomp cycles cycletype permcent