proposition: Lemma sublist_eq_same_length l k j n : length l = j * n → length k = j * n → (∀ i,i < j → sublist_lookup (i * n) n l = sublist_lookup (i * n) n k) → l = k.
proof: Proof. intros Hl Hk ?. destruct (decide (n = 0)) as [->|]. { by rewrite (nil_length_inv l), (nil_length_inv k) by lia. } apply sublist_eq with n; [by exists j|by exists j|]. intros i. destruct (decide (i < j)); [by auto|]. assert (∀ m, m = j * n → m < i * n + n). { intros ? ->. replace (i * n + n) with (S i * n) by lia. apply Nat.mul_lt_mono_pos_r; lia. } by rewrite !sublist_lookup_None by auto. Qed.
imports: stdpp(options)