proposition: Lemma split1 n i : split (i : 'I_(1 + n)) = oapp (@inr _ _) (inl _ 0) (unlift 0 i).
proof: Proof. case: unliftP => [i'|] -> /=. by rewrite -rshift1 (unsplitK (inr _ _)). by rewrite -(lshift0 n 0) (unsplitK (inl _ _)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool choice eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup) mathcomp(ssralg finalg countalg)