proposition: Lemma little_endian_to_Z_bound n bs : 0 ≤ n → Forall (λ b, 0 ≤ b < 2 ^ n) bs → 0 ≤ little_endian_to_Z n bs < 2 ^ (Z.of_nat (length bs) * n).
proof: Proof. intros ?. induction 1 as [|b bs Hb ? IH]; [done|]; simpl. apply Z.bounded_iff_bits_nonneg'; [lia|..]. { apply Z.lor_nonneg. split; [lia|]. apply Z.shiftl_nonneg. lia. } intros z' ?. rewrite Z.lor_spec. rewrite Z.bounded_iff_bits_nonneg' in Hb by lia. rewrite Hb, orb_false_l, Z.shiftl_spec by lia. apply (Z.bounded_iff_bits_nonneg' (Z.of_nat (length bs) * n)); lia. Qed.
imports: stdpp(options)