proposition: Lemma Z_to_little_endian_to_Z m n bs : m = Z.of_nat (length bs) → 0 ≤ n → Forall (λ b, 0 ≤ b < 2 ^ n) bs → Z_to_little_endian m n (little_endian_to_Z n bs) = bs.
proof: Proof. intros -> ?. induction 1 as [|b bs ? ? IH]; [done|]; simpl. rewrite Nat2Z.inj_succ, Z_to_little_endian_succ by lia. f_equal. - apply Z.bits_inj_iff'. intros z' ?. rewrite !Z.land_spec, Z.lor_spec, Z.ones_spec by lia. case_bool_decide. + rewrite andb_true_r, Z.shiftl_spec_low, orb_false_r by lia. done. + rewrite andb_false_r. symmetry. eapply (Z.bounded_iff_bits_nonneg n); lia. - rewrite <-IH at 3. f_equal. apply Z.bits_inj_iff'. intros z' ?. rewrite Z.shiftr_spec, Z.lor_spec, Z.shiftl_spec by lia. assert (Z.testbit b (z' + n) = false) as ->. { apply (Z.bounded_iff_bits_nonneg n); lia. } rewrite orb_false_l. f_equal. lia. Qed.
imports: stdpp(options)