proposition: Lemma getBit_shlBn: forall n k, k < n -> shlBn (n := n) #1 k = setBit #0 k true.
proof: Proof. move=> n k ltn_k. apply allBitsEq=> i ltn_i. case H: (i == k). * move/eqP: H ->. rewrite getBit_shlBn_true=> //. rewrite setBitThenGetSame=> //. * move/eqP: H=> H. rewrite getBit_shlBn_false=> //. rewrite setBitThenGetDistinct=> //. rewrite getBit_zero=> //. move=> Habs. rewrite Habs in H=> //. move=> Habs. by rewrite Habs in H. 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)