fact: Fixpoint splitmsb {n} : BITS n.+1 -> bool * BITS n := if n is _.+1 then fun p => let (p,b) := splitlsb p in let (c,r) := splitmsb p in (c,joinlsb(r,b)) else fun p => let (p,b) := splitlsb p in (b,p).
imports: Coq(ZArith.ZArith Strings.String) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp)