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