proposition: Lemma split_lshift m i (j : 'I_m) : split (lshift i j) = inl j.
proof: Proof. case: splitP => [j1 j1E|/= k kE]; first by congr (inl _); apply/val_eqP/eqP. by have := ltn_ord j; rewrite leqNgt kE ltnS leq_addr. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)