proposition: Lemma getBit_set_false: forall n (bs: BITS n) k x, k < n -> x < n -> getBit (andB bs (invB (shlBn #1 k))) x = (if x == k then false else getBit bs x).
proof: Proof. move=> n bs k x ? ?. case H: (x == k). - move/eqP: H=> ->. rewrite getBit_liftBinOp=> //. rewrite getBit_liftUnOp=> //. rewrite getBit_shlBn_true=> //. by apply andbF. - rewrite getBit_liftBinOp=> //. rewrite getBit_liftUnOp=> //. rewrite getBit_shlBn_false=> //; last by move/eqP: H; apply not_eq_sym. by apply andbT. 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 mathcomp(ssralg)