proposition: Lemma splitmsb_rev n : forall (b: BITS n.+1) hi (lo:BITS n), splitmsb b = (hi,lo) -> rev b = hi::rev lo.
proof: Proof. induction n => b hi lo/=. + move => [<- <-] {lo}/=. case/tupleP:b => [b u]//=. by rewrite tuple0/=. + move => H. specialize (IHn (behead_tuple b) hi). destruct (splitmsb (behead_tuple b)). injection H => [H1 H2] {H}. rewrite H2 {H2} in IHn. specialize (IHn b1 refl_equal). rewrite -H1/=. case/tupleP E: b => [b' u]/=. rewrite E/= in IHn. by rewrite 2!rev_cons IHn rcons_cons. Qed.
imports: Coq(ZArith.ZArith) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple div zmodp ssralg) ssrextra.nat ssrextra.tuple spec.spec