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