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