proposition: Lemma rshift1 n : @rshift 1 n =1 lift (0 : 'I_n.+1).
proof: Proof. by move=> i; apply: val_inj. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool choice eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup) mathcomp(ssralg finalg countalg)