proposition: Lemma rolBK n : cancel (@rolB n) (@rorB n).
proof: Proof. rewrite /cancel/rorB/rolB. case/tupleP => [b p]. case C: (splitmsb [tuple of b::p]) => [b' p']. rewrite joinlsbK. by rewrite -C splitmsbK. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div) ssrextra.tuple ssrextra.nat spec spec.properties operations mathcomp(ssralg)