proposition: Lemma Z_to_little_endian_lookup_Some m n z (i : nat) x : 0 ≤ m → 0 ≤ n → Z_to_little_endian m n z !! i = Some x ↔ Z.of_nat i < m ∧ x = Z.land (z ≫ (Z.of_nat i * n)) (Z.ones n).
proof: Proof. revert z i. induction m as [|m ? IH|] using (Z.succ_pred_induction 0); intros z i ??; [..|lia]. { destruct i; simpl; naive_solver lia. } rewrite Z_to_little_endian_succ by lia. destruct i as [|i]; simpl. { naive_solver lia. } rewrite IH, Z.shiftr_shiftr by lia. naive_solver auto with f_equal lia. Qed.
imports: stdpp(options)