proposition: Lemma splitmsb_fromNat n : forall m, splitmsb (n:=n) (fromNat m) = (odd (m %/ 2^n), fromNat m).
proof: Proof. induction n => m. + by rewrite /dropmsb/=beheadCons!theadCons expn0 divn1. + rewrite expnS. rewrite /fromNat-/fromNat/=. rewrite /joinlsb !beheadCons!theadCons fromNatHalf. specialize (IHn m./2). rewrite IHn. by rewrite -divn2 -divnMA. 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