proposition: Lemma getBit_set_true: forall n (bs: BITS n) k x, k < n -> x < n -> getBit (orB bs (shlBn #1 k)) x = (if x == k then true else getBit bs x).
proof: Proof. move=> n bs k x ? ?. case H: (x == k). - move/eqP: H=> ->. rewrite getBit_liftBinOp=> //. rewrite getBit_shlBn_true=> //. by apply orbT. - rewrite getBit_liftBinOp=> //. rewrite getBit_shlBn_false=> //; last by move/eqP: H; apply: not_eq_sym. by apply orbF. 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)