proposition: Lemma sublist_eq l k n : (n | length l) → (n | length k) → (∀ i, sublist_lookup (i * n) n l = sublist_lookup (i * n) n k) → l = k.
proof: Proof. revert l k. assert (∀ l i, n ≠ 0 → (n | length l) → ¬n * i `div` n + n ≤ length l → length l ≤ i). { intros l i ? [j ->] Hjn. apply Nat.nlt_ge; contradict Hjn. rewrite <-Nat.mul_succ_r, (Nat.mul_comm n). apply Nat.mul_le_mono_r, Nat.le_succ_l, Nat.div_lt_upper_bound; lia. } intros l k Hl Hk Hlookup. destruct (decide (n = 0)) as [->|]. { by rewrite (nil_length_inv l), (nil_length_inv k) by eauto using Nat.divide_0_l. } apply list_eq; intros i. specialize (Hlookup (i `div` n)). rewrite (Nat.mul_comm _ n) in Hlookup. unfold sublist_lookup in *; simplify_option_eq; [|by rewrite !lookup_ge_None_2 by auto]. apply (f_equal (.!! i `mod` n)) in Hlookup. by rewrite !lookup_take, !lookup_drop, <-!Nat.div_mod in Hlookup by (auto using Nat.mod_upper_bound with lia). Qed.
imports: stdpp(options)