proposition: Lemma getBit_liftUnOp: forall n op (bs : BITS n) k, k < n -> getBit (liftUnOp op bs) k = op (getBit bs k).
proof: Proof. elim=> // n IHn op /tupleP[b bs]; case=> // k le_k. + rewrite liftUnOpCons. have ->: getBit [tuple of b :: bs] k.+1 = getBit bs k by compute. have ->: getBit (consB (op b) (liftUnOp op bs)) k.+1 = getBit (liftUnOp op bs) k by compute. by apply IHn; apply le_k. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div) ssrextra.tuple ssrextra.nat spec spec.properties operations