proposition: Lemma sublist_lookup_reshape l i n m : 0 < n → length l = m * n → reshape (replicate m n) l !! i = sublist_lookup (i * n) n l.
proof: Proof. intros Hn Hl. unfold sublist_lookup. apply option_eq; intros x; split. - intros Hx. case_guard as Hi; simplify_eq/=. { f_equal. clear Hi. revert i l Hl Hx. induction m as [|m IH]; intros [|i] l ??; simplify_eq/=; auto. rewrite <-drop_drop. apply IH; rewrite ?drop_length; auto with lia. } destruct Hi. rewrite Hl, <-Nat.mul_succ_l. apply Nat.mul_le_mono_r, Nat.le_succ_l. apply lookup_lt_Some in Hx. by rewrite reshape_length, replicate_length in Hx. - intros Hx. case_guard as Hi; simplify_eq/=. revert i l Hl Hi. induction m as [|m IH]; [auto with lia|]. intros [|i] l ??; simpl; [done|]. rewrite <-drop_drop. rewrite IH; rewrite ?drop_length; auto with lia. Qed.
imports: stdpp(options)