proposition: Lemma shlBn_overflow: forall n, shlBn (n := n) #1 n = #0.
proof: Proof. move=> n. apply allBitsEq. elim: n=> [//|n IHn] k le_k. rewrite getBit_zero. case k_gtz: (k > 0). + have predk_lt_k: k.-1 < k. by rewrite -(ltn_add2r 1) !addn1 prednK //. have predk_lt_Sn: k.-1 < n.+1. by rewrite (ltn_trans (n := k))=> //. rewrite /shlBn iterS -[iter _ _ _]/(shlBn _ _) getBit_shlB=> //. rewrite getBit_shlBn_false=> //. apply/eqP. rewrite gtn_eqF //. by rewrite -(ltn_add2r 1) !addn1 prednK. + have ->: k = 0. by case: k le_k k_gtz=> //. by rewrite /shlBn iterS -[iter _ _ _]/(shlBn _ _) getBit_dropmsb=> //. 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)