proposition: Lemma getBit_shlBn_false: forall n k k', k < n -> k' < n -> k <> k' -> getBit (n := n) (shlBn #1 k) k' = false.
proof: Proof. elim=> [//|n Hn]. elim=> [|k Hk] k' le_k le_k' Hkk'. case: k' le_k' Hkk'=> [//|k' le_k' Hkk']. rewrite /= /getBit /fromNat /= -/fromNat. apply getBit_zero. case: k' le_k' Hkk'=> [|k'] le_k' Hkk'. rewrite /shlBn /=. apply getBit_shlB_0. rewrite /shlBn /= -[iter _ _ _]/(shlBn _ _). rewrite getBit_shlB /= => //. apply Hk. apply (ltn_trans (n := k.+1))=> //. apply (ltn_trans (n := k'.+1))=> //. move/eqP: Hkk'=> Hkk'. apply/eqP. by rewrite -eqSS. 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)