proposition: Lemma toNat_shlBn: forall n k, k < n -> toNat (shlBn (n := n) #1 k) = 2 ^ k.
proof: Proof. move=> n. elim=> [le_k|k IHk le_k]. + rewrite toNat_fromNat modn_small=> //. have {1}->: 1 = 2 ^ 0 by trivial. by rewrite ltn_exp2l. + rewrite toNat_shlB IHk. rewrite -muln2. have {2}->: 2 = 2 ^ 1 by trivial. rewrite -expnD addn1 modn_small // ltn_exp2l //. auto with arith. 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)