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