proposition: Lemma getBit_shlBn_true: forall n k, k < n -> getBit (n := n) (shlBn #1 k) k = true.
proof: Proof. elim=> [//|n Hn]. elim=> [|k Hk] le_k. rewrite /shlBn /=. rewrite /fromNat //. rewrite /shlBn /= getBit_shlB //=. rewrite -[iter _ _ _]/(shlBn _ _). apply Hk. by apply (ltn_trans (n := k.+1)). 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)