proposition: Lemma little_endian_to_Z_spec n bs i b : 0 ≤ i → 0 < n → Forall (λ b, 0 ≤ b < 2 ^ n) bs → bs !! Z.to_nat (i `div` n) = Some b → Z.testbit (little_endian_to_Z n bs) i = Z.testbit b (i `mod` n).
proof: Proof. intros Hi Hn Hbs. revert i Hi. induction Hbs as [|b' bs [??] ? IH]; intros i ? Hlookup; simplify_eq/=. destruct (decide (i < n)). - rewrite Z.div_small in Hlookup by lia. simplify_eq/=. rewrite Z.lor_spec, Z.shiftl_spec, Z.mod_small by lia. by rewrite (Z.testbit_neg_r _ (i - n)), orb_false_r by lia. - assert (Z.to_nat (i `div` n) = S (Z.to_nat ((i - n) `div` n))) as Hdiv. { rewrite <-Z2Nat.inj_succ by (apply Z.div_pos; lia). rewrite <-Z.add_1_r, <-Z.div_add by lia. do 2 f_equal. lia. } rewrite Hdiv in Hlookup; simplify_eq/=. rewrite Z.lor_spec, Z.shiftl_spec, IH by auto with lia. assert (Z.testbit b' i = false) as ->. { apply (Z.bounded_iff_bits_nonneg n); lia. } by rewrite <-Zminus_mod_idemp_r, Z_mod_same_full, Z.sub_0_r. Qed.
imports: stdpp(options)